Theorem 3bitr4d

Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 18-Oct-1995.)

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