Theorem 3bitr2d

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 (\psi \leftrightarrow \tau) \)
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) \)
bitrd l2 _