Theorem sylnib

A mixed syllogism inference from an implication and a biconditional. (Contributed by Wolf Lammen, 16-Dec-2013.)

Hypotheses
sylnib.1
\( \vdash \varphi \rightarrow \neg \psi \)
sylnib.2
\( \vdash \psi \leftrightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \neg \chi \)
Proof
l0
sylnib.1
\( \vdash \varphi \rightarrow \neg \psi \)
sylnib.2
biimpri _
\( \vdash \chi \rightarrow \psi \)
nsyl l0 _