Theorem simprbi

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

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