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  5288  reusv2lem2  5335  reldmtpos  8164  tz7.49  8364  omopthlem2  8575  domnsym  9016  sdomirr  9027  infensuc  9068  domnsymfi  9109  fofinf1o  9216  elfi2  9298  infdifsn  9547  carden2b  9860  alephsucdom  9970  infdif2  10100  fin4i  10189  fin45  10283  bitsf1  16357  pcmpt2  16805  symgvalstruct  19309  ufinffr  23844  eldmgm  26959  lgamucov  26975  facgam  27003  chtub  27150  cuteq1  27778  cofcutr  27868  lfgrnloop  29103  umgredgnlp  29125  clwwlkn0  30008  eupth2lem1  30198  rtelextdg2lem  33739  oddpwdc  34367  bnj1312  35070  erdszelem10  35244  heiborlem1  37850  osumcllem4N  40057  pexmidlem1N  40068  fimgmcyc  42626  fphpd  42908  0nodd  48269