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

Theorem nsyl3 125
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 123 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  126  nsyl  127  cesare  2452  cesaro  2456  pwnss  4606  reusv2lem2  4644  reldmtpos  7058  tz7.49  7239  omopthlem2  7434  domnsym  7782  sdomirr  7793  infensuc  7834  fofinf1o  7937  elfi2  8013  infdifsn  8247  carden2b  8486  alephsucdom  8595  infdif2  8725  fin4i  8813  bitsf1  14582  pcmpt2  15000  ufinffr  21102  eldmgm  24108  lgamucov  24124  facgam  24152  chtub  24301  eupath2lem1  25865  gxnval  26151  oddpwdc  29341  bnj1312  30019  erdszelem10  30075  heiborlem1  32380  osumcllem4N  33764  pexmidlem1N  33775  fphpd  35899  lfgrnloop  39750  umgredgnlp  39777  eupth2lem1  40786  0nodd  41000
  Copyright terms: Public domain W3C validator