Theorem 3bitrri

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

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