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  5310  reusv2lem2  5357  reldmtpos  8216  tz7.49  8416  omopthlem2  8627  domnsym  9073  sdomirr  9084  infensuc  9125  domnsymfi  9170  fofinf1o  9290  elfi2  9372  infdifsn  9617  carden2b  9927  alephsucdom  10039  infdif2  10169  fin4i  10258  fin45  10352  bitsf1  16423  pcmpt2  16871  symgvalstruct  19334  ufinffr  23823  eldmgm  26939  lgamucov  26955  facgam  26983  chtub  27130  cuteq1  27753  cofcutr  27839  lfgrnloop  29059  umgredgnlp  29081  clwwlkn0  29964  eupth2lem1  30154  rtelextdg2lem  33723  oddpwdc  34352  bnj1312  35055  erdszelem10  35194  heiborlem1  37812  osumcllem4N  39960  pexmidlem1N  39971  fimgmcyc  42529  fphpd  42811  0nodd  48162