Theorem impbidd

Deduce an equivalence from two implications. Double deduction associated with impbi and impbii. Deduction associated with impbid. (Contributed by Rodolfo Medina, 12-Oct-2010.)

Hypotheses
impbidd.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
impbidd.2
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow (\chi \leftrightarrow \theta) \)
Proof
l0
impbidd.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
l1
impbidd.2
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \rightarrow \chi \)
impbi
\( \vdash (\chi \rightarrow \theta) \rightarrow (\theta \rightarrow \chi) \rightarrow (\chi \leftrightarrow \theta) \)
syl6c l0 l1 _