Theorem 3bitr2rd

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

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