Theorem imbi12i

Join two logical equivalences to form equivalence of implications. (Contributed by NM, 1-Aug-1993.)

Hypotheses
imbi12i.1
\( \vdash \varphi \leftrightarrow \psi \)
imbi12i.2
\( \vdash \chi \leftrightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \chi \leftrightarrow \psi \rightarrow \theta \)
Proof
l0
imbi12i.1
\( \vdash \varphi \leftrightarrow \psi \)
l1
imbi12i.2
\( \vdash \chi \leftrightarrow \theta \)
imbi12
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow (\chi \leftrightarrow \theta) \rightarrow (\varphi \rightarrow \chi \leftrightarrow \psi \rightarrow \theta) \)
mp2 l0 l1 _