Theorem 3imtr3g

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

Hypotheses
3imtr3g.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
3imtr3g.2
\( \vdash \psi \leftrightarrow \theta \)
3imtr3g.3
\( \vdash \chi \leftrightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow \theta \rightarrow \tau \)
Proof
l0
3imtr3g.2
\( \vdash \psi \leftrightarrow \theta \)
3imtr3g.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
l2
biimtrrid l0 _
\( \vdash \varphi \rightarrow \theta \rightarrow \chi \)
3imtr3g.3
\( \vdash \chi \leftrightarrow \tau \)
imbitrdi l2 _