Theorem simplbda

Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)

Hypothesis
simplbda.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi \wedge \theta) \)
Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \theta \)
Proof
simplbda.1
biimpa _
\( \vdash \varphi \wedge \psi \rightarrow \chi \wedge \theta \)
simprd _