Theorem biimparc

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

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