Theorem nsyl 113

Description: A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)

Hypotheses

Ref	Expression
nsyl.1	⊢ (φ → ¬ ψ)
nsyl.2	⊢ (χ → ψ)

Assertion

Ref	Expression
nsyl	⊢ (φ → ¬ χ)

Proof of Theorem nsyl

Step	Hyp	Ref	Expression
1		nsyl.1	. . 3 ⊢ (φ → ¬ ψ)
2		nsyl.2	. . 3 ⊢ (χ → ψ)
3	1, 2	nsyl3 111	. 2 ⊢ (χ → ¬ φ)
4	3	con2i 112	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:  con3i  127  intnand  882  intnanrd  883  ax12  1935  ax6  2147  ax12from12o  2156  camestres  2308  camestros  2312  calemes  2319  calemos  2322  pssn2lp  3370  0nelsuc  4400  nnsucelr  4428  tfinltfin  4501  nnadjoin  4520  funun  5146  oprssdm  5612