Theorem simprld

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

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