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  5370  reusv2lem2  5417  reldmtpos  8275  tz7.49  8501  omopthlem2  8716  domnsym  9165  sdomirr  9180  infensuc  9221  domnsymfi  9266  fofinf1o  9400  elfi2  9483  infdifsn  9726  carden2b  10036  alephsucdom  10148  infdif2  10278  fin4i  10367  fin45  10461  bitsf1  16492  pcmpt2  16940  symgvalstruct  19438  symgvalstructOLD  19439  ufinffr  23958  eldmgm  27083  lgamucov  27099  facgam  27127  chtub  27274  cuteq1  27896  cofcutr  27976  lfgrnloop  29160  umgredgnlp  29182  clwwlkn0  30060  eupth2lem1  30250  rtelextdg2lem  33717  oddpwdc  34319  bnj1312  35034  erdszelem10  35168  heiborlem1  37771  osumcllem4N  39916  pexmidlem1N  39927  fimgmcyc  42489  fphpd  42772  0nodd  47893