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  pm2.65i  195  pwnss  5283  reusv2lem2  5331  reldmtpos  8178  tz7.49  8378  omopthlem2  8590  domnsym  9035  sdomirr  9046  infensuc  9087  domnsymfi  9128  fofinf1o  9236  elfi2  9321  sucprcreg  9515  infdifsn  9573  carden2b  9886  alephsucdom  9996  infdif2  10126  fin4i  10215  fin45  10309  bitsf1  16410  pcmpt2  16859  symgvalstruct  19367  ufinffr  23916  eldmgm  27007  lgamucov  27023  facgam  27051  chtub  27197  cuteq1  27831  cofcutr  27938  lfgrnloop  29216  umgredgnlp  29238  clwwlkn0  30120  eupth2lem1  30310  rtelextdg2lem  33922  oddpwdc  34550  bnj1312  35255  erdszelem10  35443  heiborlem1  38193  osumcllem4N  40466  pexmidlem1N  40477  fimgmcyc  43035  fphpd  43276  0nodd  48675