Theorem impbida

Deduce an equivalence from two implications. Variant of impbid. (Contributed by NM, 17-Feb-2007.)

Hypotheses
impbida.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
impbida.2
\( \vdash \varphi \wedge \chi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Proof
impbida.1
l1
ex _
impbida.2
ex _
impbid l1 _