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  2568  cesaro  2572  pwnss  4800  reusv2lem2  4839  reusv2lem2OLD  4840  reldmtpos  7320  tz7.49  7500  omopthlem2  7696  domnsym  8046  sdomirr  8057  infensuc  8098  fofinf1o  8201  elfi2  8280  infdifsn  8514  carden2b  8753  alephsucdom  8862  infdif2  8992  fin4i  9080  bitsf1  15111  pcmpt2  15540  ufinffr  21673  eldmgm  24682  lgamucov  24698  facgam  24726  chtub  24871  lfgrnloop  25949  umgredgnlp  25969  eupth2lem1  26978  oddpwdc  30239  bnj1312  30887  erdszelem10  30943  heiborlem1  33281  osumcllem4N  34764  pexmidlem1N  34775  fphpd  36899  0nodd  41128
 Copyright terms: Public domain W3C validator