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  5295  reusv2lem2  5342  reldmtpos  8174  tz7.49  8374  omopthlem2  8586  domnsym  9029  sdomirr  9040  infensuc  9081  domnsymfi  9122  fofinf1o  9230  elfi2  9315  infdifsn  9564  carden2b  9877  alephsucdom  9987  infdif2  10117  fin4i  10206  fin45  10300  bitsf1  16371  pcmpt2  16819  symgvalstruct  19324  ufinffr  23871  eldmgm  26986  lgamucov  27002  facgam  27030  chtub  27177  cuteq1  27805  cofcutr  27895  lfgrnloop  29147  umgredgnlp  29169  clwwlkn0  30052  eupth2lem1  30242  rtelextdg2lem  33832  oddpwdc  34460  bnj1312  35163  erdszelem10  35343  heiborlem1  37951  osumcllem4N  40158  pexmidlem1N  40169  fimgmcyc  42731  fphpd  43000  0nodd  48358