Theorem sylbb

A mixed syllogism inference from two biconditionals. (Contributed by BJ, 30-Mar-2019.)

Hypotheses
sylbb.1
\( \vdash \varphi \leftrightarrow \psi \)
sylbb.2
\( \vdash \psi \leftrightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \)
Proof
l0
sylbb.1
\( \vdash \varphi \leftrightarrow \psi \)
sylbb.2
biimpi _
\( \vdash \psi \rightarrow \chi \)
sylbi l0 _