Theorem nsyli

A negated syllogism inference. (Contributed by NM, 3-May-1994.)

Hypotheses
nsyli.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
nsyli.2
\( \vdash \theta \rightarrow \neg \chi \)
Conclusion
\( \vdash \varphi \rightarrow \theta \rightarrow \neg \psi \)
Proof
l0
nsyli.2
\( \vdash \theta \rightarrow \neg \chi \)
nsyli.1
con3d _
\( \vdash \varphi \rightarrow \neg \chi \rightarrow \neg \psi \)
syl5 l0 _