Theorem bitri

An inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.)

Hypotheses
bitri.1
\( \vdash \varphi \leftrightarrow \psi \)
bitri.2
\( \vdash \psi \leftrightarrow \chi \)
Conclusion
\( \vdash \varphi \leftrightarrow \chi \)
Proof
l0
bitri.1
\( \vdash \varphi \leftrightarrow \psi \)
bitri.2
\( \vdash \psi \leftrightarrow \chi \)
l2
sylbb l0 _
l3
bitri.1
\( \vdash \varphi \leftrightarrow \psi \)
bitri.2
\( \vdash \psi \leftrightarrow \chi \)
sylbbr l3 _
impbii l2 _