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  5244  funco  5373  fliftval  5951  ltsrprg  8027  difelfznle  10432  nelfzo  10449  iseqf1olemqk  10832  ccatsymb  11245  pfxsuffeqwrdeq  11345  pfxccatin12lem2a  11374  difsqpwdvds  12991  resmhm  13650  mhmco  13653  rhmco  14269  resrhm  14343  gausslemma2dlem1a  15877  subusgr  16216  ex-ceil  16440