Theorem nsyld

A negated syllogism deduction. (Contributed by NM, 9-Apr-2005.)

Hypotheses
nsyld.1
\( \vdash \varphi \rightarrow \psi \rightarrow \neg \chi \)
nsyld.2
\( \vdash \varphi \rightarrow \tau \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \neg \tau \)
Proof
l0
nsyld.1
\( \vdash \varphi \rightarrow \psi \rightarrow \neg \chi \)
nsyld.2
con3d _
\( \vdash \varphi \rightarrow \neg \chi \rightarrow \neg \tau \)
syld l0 _