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  5287  reusv2lem2  5334  reldmtpos  8175  tz7.49  8375  omopthlem2  8587  domnsym  9032  sdomirr  9043  infensuc  9084  domnsymfi  9125  fofinf1o  9233  elfi2  9318  infdifsn  9567  carden2b  9880  alephsucdom  9990  infdif2  10120  fin4i  10209  fin45  10303  bitsf1  16404  pcmpt2  16853  symgvalstruct  19361  ufinffr  23903  eldmgm  27003  lgamucov  27019  facgam  27047  chtub  27194  cuteq1  27828  cofcutr  27935  lfgrnloop  29213  umgredgnlp  29235  clwwlkn0  30118  eupth2lem1  30308  rtelextdg2lem  33891  oddpwdc  34519  bnj1312  35221  erdszelem10  35403  heiborlem1  38143  osumcllem4N  40416  pexmidlem1N  40427  fimgmcyc  42990  fphpd  43259  0nodd  48643