Theorem imbi12d

Deduction joining two equivalences to form equivalence of implications. (Contributed by NM, 16-May-1993.)

Hypotheses
imbi12d.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
imbi12d.2
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \tau) \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \rightarrow \theta \leftrightarrow \chi \rightarrow \tau) \)
Proof
imbi12d.1
l1
imbi1d _
\( \vdash \varphi \rightarrow (\psi \rightarrow \theta \leftrightarrow \chi \rightarrow \theta) \)
imbi12d.2
imbi2d _
\( \vdash \varphi \rightarrow (\chi \rightarrow \theta \leftrightarrow \chi \rightarrow \tau) \)
bitrd l1 _