MPE Home 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  2556  cesaro  2560  pwnss  4751  reusv2lem2  4790  reusv2lem2OLD  4791  reldmtpos  7224  tz7.49  7404  omopthlem2  7600  domnsym  7948  sdomirr  7959  infensuc  8000  fofinf1o  8103  elfi2  8180  infdifsn  8414  carden2b  8653  alephsucdom  8762  infdif2  8892  fin4i  8980  bitsf1  14952  pcmpt2  15381  ufinffr  21485  eldmgm  24465  lgamucov  24481  facgam  24509  chtub  24654  eupath2lem1  26270  oddpwdc  29549  bnj1312  30186  erdszelem10  30242  heiborlem1  32576  osumcllem4N  34059  pexmidlem1N  34070  fphpd  36194  lfgrnloop  40345  umgredgnlp  40372  eupth2lem1  41381  0nodd  41595
  Copyright terms: Public domain W3C validator