Theorem biimpar

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 \chi \rightarrow \psi \)
Proof
biimpa.1
biimprd _
imp _