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  5298  reusv2lem2  5345  reldmtpos  8178  tz7.49  8378  omopthlem2  8590  domnsym  9035  sdomirr  9046  infensuc  9087  domnsymfi  9128  fofinf1o  9236  elfi2  9321  infdifsn  9570  carden2b  9883  alephsucdom  9993  infdif2  10123  fin4i  10212  fin45  10306  bitsf1  16377  pcmpt2  16825  symgvalstruct  19330  ufinffr  23877  eldmgm  26992  lgamucov  27008  facgam  27036  chtub  27183  cuteq1  27817  cofcutr  27924  lfgrnloop  29202  umgredgnlp  29224  clwwlkn0  30107  eupth2lem1  30297  rtelextdg2lem  33885  oddpwdc  34513  bnj1312  35216  erdszelem10  35396  heiborlem1  38014  osumcllem4N  40287  pexmidlem1N  40298  fimgmcyc  42856  fphpd  43125  0nodd  48483