Theorem impbii

Infer an equivalence from an implication and its converse. Inference associated with impbi. (Contributed by NM, 29-Dec-1992.)

Hypotheses
impbii.1
\( \vdash \varphi \rightarrow \psi \)
impbii.2
\( \vdash \psi \rightarrow \varphi \)
Conclusion
\( \vdash \varphi \leftrightarrow \psi \)
Proof
l0
impbii.1
\( \vdash \varphi \rightarrow \psi \)
l1
impbii.2
\( \vdash \psi \rightarrow \varphi \)
impbi
\( \vdash (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \varphi) \rightarrow (\varphi \leftrightarrow \psi) \)
mp2 l0 l1 _