Theorem biimpa

Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.)

Hypothesis
biimpa.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Proof
biimpa.1
biimpd _
imp _