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  5267  reusv2lem2  5317  reldmtpos  8021  tz7.49  8246  omopthlem2  8450  domnsym  8839  sdomirr  8850  infensuc  8891  fofinf1o  9024  elfi2  9103  infdifsn  9345  carden2b  9656  alephsucdom  9766  infdif2  9897  fin4i  9985  fin45  10079  bitsf1  16081  pcmpt2  16522  symgvalstruct  18919  symgvalstructOLD  18920  ufinffr  22988  eldmgm  26076  lgamucov  26092  facgam  26120  chtub  26265  lfgrnloop  27398  umgredgnlp  27420  clwwlkn0  28293  eupth2lem1  28483  oddpwdc  32221  bnj1312  32938  erdszelem10  33062  cofcutr  34019  heiborlem1  35896  osumcllem4N  37900  pexmidlem1N  37911  fphpd  40554  0nodd  45252