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

Theorem nsyl3 140
 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 138 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  141  nsyl  142  nsyl2  143  pwnss  5241  reusv2lem2  5290  reldmtpos  7892  tz7.49  8073  omopthlem2  8275  domnsym  8635  sdomirr  8646  infensuc  8687  fofinf1o  8791  elfi2  8870  infdifsn  9112  carden2b  9388  alephsucdom  9497  infdif2  9624  fin4i  9712  fin45  9806  bitsf1  15787  pcmpt2  16221  symgvalstruct  18517  ufinffr  22529  eldmgm  25591  lgamucov  25607  facgam  25635  chtub  25780  lfgrnloop  26902  umgredgnlp  26924  clwwlkn0  27798  eupth2lem1  27989  oddpwdc  31605  bnj1312  32323  erdszelem10  32440  heiborlem1  35081  osumcllem4N  37087  pexmidlem1N  37098  fphpd  39404  0nodd  44068
 Copyright terms: Public domain W3C validator