Theorem nsyl3 635

Description: A negated syllogism inference. (Contributed by NM, 1-Dec-1995.) (Revised by NM, 13-Jun-2013.)

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 9	. 2 ⊢ (𝜒 → (𝜑 → ¬ 𝜓))
4	1, 3	mt2d 634	1 ⊢ (𝜒 → ¬ 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 623  ax-in2 624

This theorem is used by:  con2i  636  nsyl  637  pm2.65i  648  cesare  2191  cesaro  2195  pwnss  4296  sucprcreg  4696  reg3exmidlemwe  4726  reldmtpos  6524  snexxph  7267  elfi2  7306  ismkvnex  7496  fzn  10457  seq3f1olemqsum  10965  pcmpt2  13146  elply2  15927  chtqub  16257  umgredgnlp  16559  clwwlkn0  16815