Theorem sylbb2

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

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