Theorem simpld

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

	Ref	Expression
Hypothesis	simpld.1	|- ( ph -> ( ps /\ ch ) )
Assertion	simpld	|- ( ph -> ps )

Proof

Step	Hyp	Ref	Expression
1		simpld.1	|- ( ph -> ( ps /\ ch ) )
2		simpl	|- ( ( ps /\ ch ) -> ps )
3	1 2	syl	|- ( ph -> ps )