Theorem simplrd

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

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