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

Theorem nsyl3 135
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 133 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  136  nsyl  137  cesare  2718  cesaro  2722  pwnss  4962  reusv2lem2  5000  reldmtpos  7513  tz7.49  7694  omopthlem2  7891  domnsym  8243  sdomirr  8254  infensuc  8295  fofinf1o  8398  elfi2  8477  infdifsn  8719  carden2b  8994  alephsucdom  9103  infdif2  9235  fin4i  9323  bitsf1  15377  pcmpt2  15805  ufinffr  21954  eldmgm  24970  lgamucov  24986  facgam  25014  chtub  25159  lfgrnloop  26242  umgredgnlp  26265  clwwlkn0  27183  eupth2lem1  27399  oddpwdc  30757  bnj1312  31465  erdszelem10  31521  heiborlem1  33943  osumcllem4N  35768  pexmidlem1N  35779  fphpd  37907  0nodd  42339
  Copyright terms: Public domain W3C validator