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  5235  funco  5364  fliftval  5936  ltsrprg  7957  difelfznle  10360  nelfzo  10377  iseqf1olemqk  10759  ccatsymb  11169  pfxsuffeqwrdeq  11269  pfxccatin12lem2a  11298  difsqpwdvds  12901  resmhm  13560  mhmco  13563  rhmco  14178  resrhm  14252  gausslemma2dlem1a  15777  ex-ceil  16258