Theorem 3imtr4d

More general version of 3imtr4i. Useful for converting conditional definitions in a formula. (Contributed by NM, 26-Oct-1995.)

Hypotheses
3imtr4d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
3imtr4d.2
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \psi) \)
3imtr4d.3
\( \vdash \varphi \rightarrow (\tau \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow \theta \rightarrow \tau \)
Proof
l0
3imtr4d.2
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \psi) \)
l1
3imtr4d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
3imtr4d.3
\( \vdash \varphi \rightarrow (\tau \leftrightarrow \chi) \)
sylibrd l1 _
\( \vdash \varphi \rightarrow \psi \rightarrow \tau \)
sylbid l0 _