Theorem impbid1

Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.)

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