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

Theorem nsyl3 131
 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 129 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  132  nsyl  133  cesare  2461  cesaro  2465  pwnss  4655  reusv2lem2  4694  reusv2lem2OLD  4695  reldmtpos  7121  tz7.49  7302  omopthlem2  7498  domnsym  7846  sdomirr  7857  infensuc  7898  fofinf1o  8001  elfi2  8078  infdifsn  8312  carden2b  8551  alephsucdom  8660  infdif2  8790  fin4i  8878  bitsf1  14877  pcmpt2  15317  ufinffr  21444  eldmgm  24436  lgamucov  24452  facgam  24480  chtub  24627  eupath2lem1  26243  oddpwdc  29551  bnj1312  30226  erdszelem10  30282  heiborlem1  32655  osumcllem4N  34138  pexmidlem1N  34149  fphpd  36273  lfgrnloop  40442  umgredgnlp  40469  eupth2lem1  41478  0nodd  41692
 Copyright terms: Public domain W3C validator