Theorem 3bitr3rd

Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)

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 (\tau \leftrightarrow \theta) \)
Proof
l0
3bitr3d.3
\( \vdash \varphi \rightarrow (\chi \leftrightarrow \tau) \)
l1
3bitr3d.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
3bitr3d.2
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \theta) \)
bitr3d l1 _
\( \vdash \varphi \rightarrow (\chi \leftrightarrow \theta) \)
bitr3d l0 _