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  2756  cesaroOLD  2764  pwnss  5052  reusv2lem2  5099  reldmtpos  7625  tz7.49  7806  omopthlem2  8003  domnsym  8355  sdomirr  8366  infensuc  8407  fofinf1o  8510  elfi2  8589  infdifsn  8831  carden2b  9106  alephsucdom  9215  infdif2  9347  fin4i  9435  bitsf1  15541  pcmpt2  15968  ufinffr  22103  eldmgm  25161  lgamucov  25177  facgam  25205  chtub  25350  lfgrnloop  26423  umgredgnlp  26446  clwwlkn0  27370  eupth2lem1  27595  oddpwdc  30961  bnj1312  31672  erdszelem10  31728  heiborlem1  34152  osumcllem4N  36034  pexmidlem1N  36045  fphpd  38224  0nodd  42657