Theorem sylbb1

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

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