Theorem mulcom 8204

Description: Alias for ax-mulcom 8176, for naming consistency with mulcomi 8228. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
mulcom	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )

Proof of Theorem mulcom

Step	Hyp	Ref	Expression
1		ax-mulcom 8176	1 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1398   e. wcel 2202  (class class class)co 6028   CCcc 8073   x. cmul 8080

This theorem was proved from axioms:  ax-mulcom 8176

This theorem is referenced by:  adddir  8213  mullid  8220  mulcomi  8228  mulcomd  8243  mul12  8350  mul32  8351  mul31  8352  muladd  8605  subdir  8607  mul01  8610  mulneg2  8617  recextlem1  8873  divmulap3  8899  div23ap  8913  div13ap  8915  div12ap  8916  divmulasscomap  8918  divcanap4  8921  divmul13ap  8937  divmul24ap  8938  divcanap7  8943  div2negap  8957  prodgt02  9075  prodge02  9077  ltmul2  9078  lemul2  9079  lemul2a  9081  ltmulgt12  9087  lemulge12  9089  ltmuldiv2  9097  ltdivmul2  9100  ledivmul2  9102  lemuldiv2  9104  times2  9314  modqcyc2  10668  subsq  10954  cjmulrcl  11510  imval2  11517  abscj  11675  sqabsadd  11678  sqabssub  11679  prod3fmul  12165  prodmodclem3  12199  efcllemp  12282  efexp  12306  sinmul  12368  demoivreALT  12398  dvdsmul1  12437  odd2np1lem  12496  odd2np1  12497  opeo  12521  omeo  12522  modgcd  12625  dvdsgcd  12646  gcdmultiple  12654  coprmdvds  12727  coprmdvds2  12728  qredeq  12731  modprm0  12890  modprmn0modprm0  12892  coprimeprodsq2  12894  cncrng  14648  cnfldui  14668  ef2kpi  15600  sinperlem  15602  sinmpi  15609  cosmpi  15610  sinppi  15611  cosppi  15612  cxpcom  15732  perfectlem1  15796  perfectlem2  15797  perfect  15798  lgsdir2lem4  15833  lgsdir2  15835  lgsquadlem2  15880  lgsquad2  15885