Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nsyl3 Structured version   Visualization version   GIF version

Theorem nsyl3 133
 Description: A negated syllogism inference. (Contributed by NM, 1-Dec-1995.)
Hypotheses
Ref Expression
nsyl3.1 (𝜑 → ¬ 𝜓)
nsyl3.2 (𝜒𝜓)
Assertion
Ref Expression
nsyl3 (𝜒 → ¬ 𝜑)

Proof of Theorem nsyl3
StepHypRef Expression
1 nsyl3.2 . 2 (𝜒𝜓)
2 nsyl3.1 . . 3 (𝜑 → ¬ 𝜓)
32a1i 11 . 2 (𝜒 → (𝜑 → ¬ 𝜓))
41, 3mt2d 131 1 (𝜒 → ¬ 𝜑)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem is referenced by:  con2i  134  nsyl  135  cesare  2699  cesaro  2703  pwnss  4971  reusv2lem2  5010  reusv2lem2OLD  5011  reldmtpos  7521  tz7.49  7701  omopthlem2  7897  domnsym  8243  sdomirr  8254  infensuc  8295  fofinf1o  8398  elfi2  8477  infdifsn  8719  carden2b  8975  alephsucdom  9084  infdif2  9216  fin4i  9304  bitsf1  15362  pcmpt2  15791  ufinffr  21926  eldmgm  24939  lgamucov  24955  facgam  24983  chtub  25128  lfgrnloop  26211  umgredgnlp  26233  clwwlkn0  27147  eupth2lem1  27362  oddpwdc  30717  bnj1312  31425  erdszelem10  31481  heiborlem1  33915  osumcllem4N  35740  pexmidlem1N  35751  fphpd  37874  0nodd  42312
 Copyright terms: Public domain W3C validator