Theorem anim1d

Description: Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994)

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

Proof

Step	Hyp	Ref	Expression
1		anim1d.1	|- ( ph -> ( ps -> ch ) )
2		idd	|- ( ph -> ( th -> th ) )
3	1 2	anim12d	|- ( ph -> ( ( ps /\ th ) -> ( ch /\ th ) ) )