Theorem impbid2

Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) (Proof shortened by Wolf Lammen, 27-Sep-2013.)

Hypotheses
impbid2.1
\( \vdash \psi \rightarrow \chi \)
impbid2.2
\( \vdash \varphi \rightarrow \chi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Proof
l0
impbid2.2
impbid2.1
impbid1 l0 _
bicomd _