Theorem 3imtr4g

More general version of 3imtr4i. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)

Hypotheses
3imtr4g.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
3imtr4g.2
\( \vdash \theta \leftrightarrow \psi \)
3imtr4g.3
\( \vdash \tau \leftrightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \theta \rightarrow \tau \)
Proof
l0
3imtr4g.2
\( \vdash \theta \leftrightarrow \psi \)
3imtr4g.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
l2
biimtrid l0 _
\( \vdash \varphi \rightarrow \theta \rightarrow \chi \)
3imtr4g.3
\( \vdash \tau \leftrightarrow \chi \)
imbitrrdi l2 _