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

Theorem nsyl3 136
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 134 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  137  nsyl  138  cesareOLD  2757  cesaroOLD  2765  pwnss  5053  reusv2lem2  5100  reldmtpos  7626  tz7.49  7807  omopthlem2  8004  domnsym  8356  sdomirr  8367  infensuc  8408  fofinf1o  8511  elfi2  8590  infdifsn  8832  carden2b  9107  alephsucdom  9216  infdif2  9348  fin4i  9436  bitsf1  15542  pcmpt2  15969  ufinffr  22104  eldmgm  25162  lgamucov  25178  facgam  25206  chtub  25351  lfgrnloop  26424  umgredgnlp  26447  clwwlkn0  27371  eupth2lem1  27596  oddpwdc  30962  bnj1312  31673  erdszelem10  31729  heiborlem1  34153  osumcllem4N  36035  pexmidlem1N  36046  fphpd  38225  0nodd  42658
  Copyright terms: Public domain W3C validator