Theorem 3bitr3ri

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

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