Theorem nsyl3 139

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 137	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  140  nsyl  141  nsyl2  142  pm2.65i  196  pwnss  5323  reusv2lem2  5371  reldmtpos  8230  tz7.49  8432  omopthlem2  8646  domnsym  9091  sdomirr  9102  infensuc  9143  domnsymfi  9184  fofinf1o  9289  elfi2  9374  sucprcreg  9568  infdifsn  9626  carden2b  9953  alephsucdom  10063  infdif2  10192  fin4i  10282  fin45  10376  bitsf1  16504  pcmpt2  16953  symgvalstruct  19467  ufinffr  24055  eldmgm  27152  lgamucov  27168  facgam  27196  chtub  27342  cuteq1  27976  cofcutr  28083  lfgrnloop  29416  umgredgnlp  29438  clwwlkn0  30320  eupth2lem1  30510  rtelextdg2lem  34061  oddpwdc  34689  bnj1312  35391  erdszelem10  35625  heiborlem1  38384  osumcllem4N  40657  pexmidlem1N  40668  fimgmcyc  43228  fphpd  43469  0nodd  48858