Theorem 3bitr4ri

A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.)

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