Theorem 3bitr4i

A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.)

Hypotheses
3bitr4i.1
\( \vdash \varphi \leftrightarrow \psi \)
3bitr4i.2
\( \vdash \chi \leftrightarrow \varphi \)
3bitr4i.3
\( \vdash \theta \leftrightarrow \psi \)
Conclusion
\( \vdash \chi \leftrightarrow \theta \)
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 \)
bitri l0 _