Theorem nsyl

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

Hypotheses
nsyl.1
\( \vdash \varphi \rightarrow \neg \psi \)
nsyl.2
\( \vdash \chi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow \neg \chi \)
Proof
l0
nsyl.1
\( \vdash \varphi \rightarrow \neg \psi \)
nsyl.2
\( \vdash \chi \rightarrow \psi \)
nsyl3 l0 _
con2i _