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  5301  reusv2lem2  5348  reldmtpos  8188  tz7.49  8388  omopthlem2  8600  domnsym  9045  sdomirr  9056  infensuc  9097  domnsymfi  9138  fofinf1o  9246  elfi2  9331  infdifsn  9580  carden2b  9893  alephsucdom  10003  infdif2  10133  fin4i  10222  fin45  10316  bitsf1  16387  pcmpt2  16835  symgvalstruct  19343  ufinffr  23890  eldmgm  27005  lgamucov  27021  facgam  27049  chtub  27196  cuteq1  27830  cofcutr  27937  lfgrnloop  29216  umgredgnlp  29238  clwwlkn0  30121  eupth2lem1  30311  rtelextdg2lem  33910  oddpwdc  34538  bnj1312  35240  erdszelem10  35422  heiborlem1  38091  osumcllem4N  40364  pexmidlem1N  40375  fimgmcyc  42933  fphpd  43202  0nodd  48559