Theorem 3imtr3d

More general version of 3imtr3i. Useful for converting conditional definitions in a formula. (Contributed by NM, 8-Apr-1996.)

Hypotheses
3imtr3d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
3imtr3d.2
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \theta) \)
3imtr3d.3
\( \vdash \varphi \rightarrow (\chi \leftrightarrow \tau) \)
Conclusion
\( \vdash \varphi \rightarrow \theta \rightarrow \tau \)
Proof
l0
3imtr3d.2
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \theta) \)
l1
3imtr3d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
3imtr3d.3
\( \vdash \varphi \rightarrow (\chi \leftrightarrow \tau) \)
sylibd l1 _
\( \vdash \varphi \rightarrow \psi \rightarrow \tau \)
sylbird l0 _