Theorem simplbi2

Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.)

Hypothesis
simplbi2.1
\( \vdash \varphi \leftrightarrow \psi \wedge \chi \)
Conclusion
\( \vdash \psi \rightarrow \chi \rightarrow \varphi \)
Proof
simplbi2.1
biimpri _
ex _