Theorem 3bitri

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

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