Theorem 3bitr3d

Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.)

Hypotheses
3bitr3d.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
3bitr3d.2
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \theta) \)
3bitr3d.3
\( \vdash \varphi \rightarrow (\chi \leftrightarrow \tau) \)
Conclusion
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \tau) \)
Proof
l0
3bitr3d.2
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \theta) \)
3bitr3d.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
l2
bitr3d l0 _
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \chi) \)
3bitr3d.3
\( \vdash \varphi \rightarrow (\chi \leftrightarrow \tau) \)
bitrd l2 _