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  5322  reusv2lem2  5369  reldmtpos  8233  tz7.49  8459  omopthlem2  8672  domnsym  9113  sdomirr  9128  infensuc  9169  domnsymfi  9214  fofinf1o  9344  elfi2  9426  infdifsn  9671  carden2b  9981  alephsucdom  10093  infdif2  10223  fin4i  10312  fin45  10406  bitsf1  16465  pcmpt2  16913  symgvalstruct  19378  ufinffr  23867  eldmgm  26984  lgamucov  27000  facgam  27028  chtub  27175  cuteq1  27798  cofcutr  27884  lfgrnloop  29104  umgredgnlp  29126  clwwlkn0  30009  eupth2lem1  30199  rtelextdg2lem  33760  oddpwdc  34386  bnj1312  35089  erdszelem10  35222  heiborlem1  37835  osumcllem4N  39978  pexmidlem1N  39989  fimgmcyc  42557  fphpd  42839  0nodd  48145