Theorem anim12dan

Description: Conjoin antecedents and consequents in a deduction. (Contributed by Jeff Madsen, 16-Jun-2011)

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

Proof

Step	Hyp	Ref	Expression
1		anim12dan.1	|- ( ( ph /\ ps ) -> ch )
2		anim12dan.2	|- ( ( ph /\ th ) -> ta )
3	1	ex	|- ( ph -> ( ps -> ch ) )
4	2	ex	|- ( ph -> ( th -> ta ) )
5	3 4	anim12d	|- ( ph -> ( ( ps /\ th ) -> ( ch /\ ta ) ) )
6	5	imp	|- ( ( ph /\ ( ps /\ th ) ) -> ( ch /\ ta ) )