Theorem anim12ci 339

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

Hypotheses

Ref	Expression
anim12i.1	|- ( ph -> ps )
anim12i.2	|- ( ch -> th )

Assertion

Ref	Expression
anim12ci	|- ( ( ph /\ ch ) -> ( th /\ ps ) )

Proof of Theorem anim12ci

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

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  anim1ci  341  dfco2a  5202  funco  5330  fliftval  5892  ltsrprg  7895  difelfznle  10292  nelfzo  10309  iseqf1olemqk  10689  ccatsymb  11096  pfxsuffeqwrdeq  11189  pfxccatin12lem2a  11218  difsqpwdvds  12776  resmhm  13434  mhmco  13437  rhmco  14051  resrhm  14125  gausslemma2dlem1a  15650  ex-ceil  15862