Theorem anim12d

Description: Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994) (Proof shortened by Wolf Lammen, 18-Dec-2013)

	Ref	Expression
Hypotheses	anim12d.1	|- ( ph -> ( ps -> ch ) )
	anim12d.2	|- ( ph -> ( th -> ta ) )
Assertion	anim12d	|- ( ph -> ( ( ps /\ th ) -> ( ch /\ ta ) ) )

Proof

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