Theorem anim12ci

Description: Variant of anim12i with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

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

Proof

Step	Hyp	Ref	Expression
1		anim12i.1	|- ( ph -> ps )
2		anim12i.2	|- ( ch -> th )
3	2 1	anim12i	|- ( ( ch /\ ph ) -> ( th /\ ps ) )
4	3	ancoms	|- ( ( ph /\ ch ) -> ( th /\ ps ) )