Theorem 3bitrd

Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.)

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