Theorem simprrd

Deduction form of simprr, eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

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