Theorem 3bitr2ri

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 \theta \leftrightarrow \varphi \)
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 \)
bitr2i l2 _