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

Theorem nsyl3 138
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 136 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  139  nsyl  140  nsyl2  141  pwnss  5339  reusv2lem2  5387  reldmtpos  8214  tz7.49  8440  omopthlem2  8655  domnsym  9095  sdomirr  9110  infensuc  9151  domnsymfi  9199  fofinf1o  9323  elfi2  9405  infdifsn  9648  carden2b  9958  alephsucdom  10070  infdif2  10201  fin4i  10289  fin45  10383  bitsf1  16384  pcmpt2  16825  symgvalstruct  19306  symgvalstructOLD  19307  ufinffr  23755  eldmgm  26870  lgamucov  26886  facgam  26914  chtub  27061  cuteq1  27682  cofcutr  27760  lfgrnloop  28854  umgredgnlp  28876  clwwlkn0  29750  eupth2lem1  29940  oddpwdc  33842  bnj1312  34558  erdszelem10  34680  heiborlem1  37169  osumcllem4N  39320  pexmidlem1N  39331  fphpd  42043  0nodd  47033
  Copyright terms: Public domain W3C validator