Theorem simpld

Deduction eliminating a conjunct. A translation of natural deduction rule /\ EL ( /\ elimination left), see [natded]. (Contributed by NM, 26-May-1993.)

Hypothesis
simpld.1
\( \vdash \varphi \rightarrow \psi \wedge \chi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \)
Proof
l0
simpld.1
\( \vdash \varphi \rightarrow \psi \wedge \chi \)
simpl
\( \vdash \psi \wedge \chi \rightarrow \psi \)
syl l0 _