Theorem anim12d1

Description: Variant of anim12d where the second implication does not depend on the antecedent. (Contributed by Rodolfo Medina, 12-Oct-2010)

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

Proof

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