Theorem 3bitr4rd

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

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