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  5352  reusv2lem2  5399  reldmtpos  8259  tz7.49  8485  omopthlem2  8698  domnsym  9139  sdomirr  9154  infensuc  9195  domnsymfi  9240  fofinf1o  9372  elfi2  9454  infdifsn  9697  carden2b  10007  alephsucdom  10119  infdif2  10249  fin4i  10338  fin45  10432  bitsf1  16483  pcmpt2  16931  symgvalstruct  19414  symgvalstructOLD  19415  ufinffr  23937  eldmgm  27065  lgamucov  27081  facgam  27109  chtub  27256  cuteq1  27878  cofcutr  27958  lfgrnloop  29142  umgredgnlp  29164  clwwlkn0  30047  eupth2lem1  30237  rtelextdg2lem  33767  oddpwdc  34356  bnj1312  35072  erdszelem10  35205  heiborlem1  37818  osumcllem4N  39961  pexmidlem1N  39972  fimgmcyc  42544  fphpd  42827  0nodd  48086