MPE Home 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  4790  reusv2lem2  4829  reusv2lem2OLD  4830  reldmtpos  7305  tz7.49  7485  omopthlem2  7681  domnsym  8030  sdomirr  8041  infensuc  8082  fofinf1o  8185  elfi2  8264  infdifsn  8498  carden2b  8737  alephsucdom  8846  infdif2  8976  fin4i  9064  bitsf1  15092  pcmpt2  15521  ufinffr  21643  eldmgm  24648  lgamucov  24664  facgam  24692  chtub  24837  lfgrnloop  25915  umgredgnlp  25935  eupth2lem1  26944  oddpwdc  30197  bnj1312  30834  erdszelem10  30890  heiborlem1  33242  osumcllem4N  34725  pexmidlem1N  34736  fphpd  36860  0nodd  41098
  Copyright terms: Public domain W3C validator