Theorem sylbir

A mixed syllogism inference from a biconditional and an implication. (Contributed by NM, 3-Jan-1993.)

Hypotheses
sylbir.1
\( \vdash \psi \leftrightarrow \varphi \)
sylbir.2
\( \vdash \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \)
Proof
sylbir.1
l1
biimpri _
\( \vdash \varphi \rightarrow \psi \)
sylbir.2
\( \vdash \psi \rightarrow \chi \)
syl l1 _