Theorem 3bitrrd

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

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