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  5293  reusv2lem2  5341  reldmtpos  8184  tz7.49  8384  omopthlem2  8596  domnsym  9041  sdomirr  9052  infensuc  9093  domnsymfi  9134  fofinf1o  9242  elfi2  9327  sucprcreg  9520  infdifsn  9578  carden2b  9891  alephsucdom  10001  infdif2  10131  fin4i  10220  fin45  10314  bitsf1  16415  pcmpt2  16864  symgvalstruct  19372  ufinffr  23894  eldmgm  26985  lgamucov  27001  facgam  27029  chtub  27175  cuteq1  27809  cofcutr  27916  lfgrnloop  29194  umgredgnlp  29216  clwwlkn0  30098  eupth2lem1  30288  rtelextdg2lem  33870  oddpwdc  34498  bnj1312  35200  erdszelem10  35382  heiborlem1  38132  osumcllem4N  40405  pexmidlem1N  40416  fimgmcyc  42979  fphpd  43244  0nodd  48646