Theorem simplbi

Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)

Hypothesis
simplbi.1
\( \vdash \varphi \leftrightarrow \psi \wedge \chi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \)
Proof
simplbi.1
biimpi _
\( \vdash \varphi \rightarrow \psi \wedge \chi \)
simpld _