Theorem impbid

Deduce an equivalence from two implications. Deduction associated with impbi and impbii. (Contributed by NM, 24-Jan-1993.) Prove it from impbid21d. (Revised by Wolf Lammen, 3-Nov-2012.)

Hypotheses
impbid.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
impbid.2
\( \vdash \varphi \rightarrow \chi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Proof
l0
impbid.1
impbid.2
impbid21d l0 _
pm2.43i _