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  5302  reusv2lem2  5349  reldmtpos  8190  tz7.49  8390  omopthlem2  8601  domnsym  9044  sdomirr  9055  infensuc  9096  domnsymfi  9141  fofinf1o  9259  elfi2  9341  infdifsn  9586  carden2b  9896  alephsucdom  10008  infdif2  10138  fin4i  10227  fin45  10321  bitsf1  16392  pcmpt2  16840  symgvalstruct  19311  ufinffr  23849  eldmgm  26965  lgamucov  26981  facgam  27009  chtub  27156  cuteq1  27783  cofcutr  27872  lfgrnloop  29105  umgredgnlp  29127  clwwlkn0  30007  eupth2lem1  30197  rtelextdg2lem  33709  oddpwdc  34338  bnj1312  35041  erdszelem10  35180  heiborlem1  37798  osumcllem4N  39946  pexmidlem1N  39957  fimgmcyc  42515  fphpd  42797  0nodd  48151