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

Step	Hyp	Ref	Expression
1		nsyl3.2	. 2 ⊢ (𝜒 → 𝜓)
2		nsyl3.1	. . 3 ⊢ (𝜑 → ¬ 𝜓)
3	2	a1i 11	. 2 ⊢ (𝜒 → (𝜑 → ¬ 𝜓))
4	1, 3	mt2d 136	1 ⊢ (𝜒 → ¬ 𝜑)

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  5291  reusv2lem2  5338  reldmtpos  8167  tz7.49  8367  omopthlem2  8578  domnsym  9020  sdomirr  9031  infensuc  9072  domnsymfi  9114  fofinf1o  9222  elfi2  9304  infdifsn  9553  carden2b  9863  alephsucdom  9973  infdif2  10103  fin4i  10192  fin45  10286  bitsf1  16357  pcmpt2  16805  symgvalstruct  19276  ufinffr  23814  eldmgm  26930  lgamucov  26946  facgam  26974  chtub  27121  cuteq1  27748  cofcutr  27837  lfgrnloop  29070  umgredgnlp  29092  clwwlkn0  29972  eupth2lem1  30162  rtelextdg2lem  33699  oddpwdc  34328  bnj1312  35031  erdszelem10  35183  heiborlem1  37801  osumcllem4N  39948  pexmidlem1N  39959  fimgmcyc  42517  fphpd  42799  0nodd  48164