Theorem nsyl3 136

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 134	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  137  nsyl  138  cesareOLD  2757  cesaroOLD  2765  pwnss  5053  reusv2lem2  5100  reldmtpos  7626  tz7.49  7807  omopthlem2  8004  domnsym  8356  sdomirr  8367  infensuc  8408  fofinf1o  8511  elfi2  8590  infdifsn  8832  carden2b  9107  alephsucdom  9216  infdif2  9348  fin4i  9436  bitsf1  15542  pcmpt2  15969  ufinffr  22104  eldmgm  25162  lgamucov  25178  facgam  25206  chtub  25351  lfgrnloop  26424  umgredgnlp  26447  clwwlkn0  27371  eupth2lem1  27596  oddpwdc  30962  bnj1312  31673  erdszelem10  31729  heiborlem1  34153  osumcllem4N  36035  pexmidlem1N  36046  fphpd  38225  0nodd  42658