Theorem 3bitr2i

A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)

Hypotheses
3bitr2i.1
\( \vdash \varphi \leftrightarrow \psi \)
3bitr2i.2
\( \vdash \chi \leftrightarrow \psi \)
3bitr2i.3
\( \vdash \chi \leftrightarrow \theta \)
Conclusion
\( \vdash \varphi \leftrightarrow \theta \)
Proof
l0
3bitr2i.1
\( \vdash \varphi \leftrightarrow \psi \)
3bitr2i.2
\( \vdash \chi \leftrightarrow \psi \)
l2
bitr4i l0 _
\( \vdash \varphi \leftrightarrow \chi \)
3bitr2i.3
\( \vdash \chi \leftrightarrow \theta \)
bitri l2 _