Theorem 3bitr3i

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

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