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

Theorem nsyl3 132
 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 130 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  133  nsyl  134  cesare  2557  cesaro  2561  pwnss  4756  reusv2lem2  4795  reusv2lem2OLD  4796  reldmtpos  7247  tz7.49  7427  omopthlem2  7623  domnsym  7971  sdomirr  7982  infensuc  8023  fofinf1o  8126  elfi2  8203  infdifsn  8437  carden2b  8676  alephsucdom  8785  infdif2  8915  fin4i  9003  bitsf1  15006  pcmpt2  15435  ufinffr  21543  eldmgm  24548  lgamucov  24564  facgam  24592  chtub  24737  lfgrnloop  25791  umgredgnlp  25818  eupath2lem1  26504  oddpwdc  29743  bnj1312  30380  erdszelem10  30436  heiborlem1  32780  osumcllem4N  34263  pexmidlem1N  34274  fphpd  36398  eupth2lem1  41386  0nodd  41600
 Copyright terms: Public domain W3C validator