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  5272  reusv2lem2  5322  reldmtpos  8050  tz7.49  8276  omopthlem2  8490  domnsym  8886  sdomirr  8901  infensuc  8942  domnsymfi  8986  fofinf1o  9094  elfi2  9173  infdifsn  9415  carden2b  9725  alephsucdom  9835  infdif2  9966  fin4i  10054  fin45  10148  bitsf1  16153  pcmpt2  16594  symgvalstruct  19004  symgvalstructOLD  19005  ufinffr  23080  eldmgm  26171  lgamucov  26187  facgam  26215  chtub  26360  lfgrnloop  27495  umgredgnlp  27517  clwwlkn0  28392  eupth2lem1  28582  oddpwdc  32321  bnj1312  33038  erdszelem10  33162  cofcutr  34092  heiborlem1  35969  osumcllem4N  37973  pexmidlem1N  37984  fphpd  40638  0nodd  45364