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  pm2.65i  195  pwnss  5310  reusv2lem2  5358  reldmtpos  8216  tz7.49  8418  omopthlem2  8632  domnsym  9077  sdomirr  9088  infensuc  9129  domnsymfi  9170  fofinf1o  9277  elfi2  9362  sucprcreg  9556  infdifsn  9614  carden2b  9927  alephsucdom  10037  infdif2  10167  fin4i  10257  fin45  10351  bitsf1  16482  pcmpt2  16931  symgvalstruct  19439  ufinffr  23991  eldmgm  27088  lgamucov  27104  facgam  27132  chtub  27278  cuteq1  27912  cofcutr  28019  lfgrnloop  29328  umgredgnlp  29350  clwwlkn0  30232  eupth2lem1  30422  rtelextdg2lem  34025  oddpwdc  34653  bnj1312  35355  erdszelem10  35555  heiborlem1  38315  osumcllem4N  40588  pexmidlem1N  40599  fimgmcyc  43157  fphpd  43398  0nodd  48797