Theorem mulcom 7773

Description: Alias for ax-mulcom 7745, for naming consistency with mulcomi 7796. (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 7745	1 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1332   e. wcel 1481  (class class class)co 5782   CCcc 7642   x. cmul 7649

This theorem was proved from axioms:  ax-mulcom 7745

This theorem is referenced by:  adddir  7781  mulid2  7788  mulcomi  7796  mulcomd  7811  mul12  7915  mul32  7916  mul31  7917  muladd  8170  subdir  8172  mul01  8175  mulneg2  8182  recextlem1  8436  divmulap3  8461  div23ap  8475  div13ap  8477  div12ap  8478  divmulasscomap  8480  divcanap4  8483  divmul13ap  8499  divmul24ap  8500  divcanap7  8505  div2negap  8519  prodgt02  8635  prodge02  8637  ltmul2  8638  lemul2  8639  lemul2a  8641  ltmulgt12  8647  lemulge12  8649  ltmuldiv2  8657  ltdivmul2  8660  ledivmul2  8662  lemuldiv2  8664  times2  8873  modqcyc2  10164  subsq  10430  cjmulrcl  10691  imval2  10698  abscj  10856  sqabsadd  10859  sqabssub  10860  prod3fmul  11342  prodmodclem3  11376  efcllemp  11401  efexp  11425  sinmul  11487  demoivreALT  11516  dvdsmul1  11551  odd2np1lem  11605  odd2np1  11606  opeo  11630  omeo  11631  modgcd  11715  dvdsgcd  11736  gcdmultiple  11744  coprmdvds  11809  coprmdvds2  11810  qredeq  11813  ef2kpi  12935  sinperlem  12937  sinmpi  12944  cosmpi  12945  sinppi  12946  cosppi  12947  cxpcom  13065