Theorem sylnbir

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

Hypotheses
sylnbir.1
\( \vdash \psi \leftrightarrow \varphi \)
sylnbir.2
\( \vdash \neg \psi \rightarrow \chi \)
Conclusion
\( \vdash \neg \varphi \rightarrow \chi \)
Proof
sylnbir.1
l1
bicomi _
\( \vdash \varphi \leftrightarrow \psi \)
sylnbir.2
\( \vdash \neg \psi \rightarrow \chi \)
sylnbi l1 _