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  5228  funco  5357  fliftval  5923  ltsrprg  7930  difelfznle  10327  nelfzo  10344  iseqf1olemqk  10724  ccatsymb  11132  pfxsuffeqwrdeq  11225  pfxccatin12lem2a  11254  difsqpwdvds  12856  resmhm  13515  mhmco  13518  rhmco  14132  resrhm  14206  gausslemma2dlem1a  15731  ex-ceil  16048