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  5307  reusv2lem2  5354  reldmtpos  8213  tz7.49  8413  omopthlem2  8624  domnsym  9067  sdomirr  9078  infensuc  9119  domnsymfi  9164  fofinf1o  9283  elfi2  9365  infdifsn  9610  carden2b  9920  alephsucdom  10032  infdif2  10162  fin4i  10251  fin45  10345  bitsf1  16416  pcmpt2  16864  symgvalstruct  19327  ufinffr  23816  eldmgm  26932  lgamucov  26948  facgam  26976  chtub  27123  cuteq1  27746  cofcutr  27832  lfgrnloop  29052  umgredgnlp  29074  clwwlkn0  29957  eupth2lem1  30147  rtelextdg2lem  33716  oddpwdc  34345  bnj1312  35048  erdszelem10  35187  heiborlem1  37805  osumcllem4N  39953  pexmidlem1N  39964  fimgmcyc  42522  fphpd  42804  0nodd  48158