Theorem mulcom 8053

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1372   e. wcel 2175  (class class class)co 5943   CCcc 7922   x. cmul 7929

This theorem was proved from axioms:  ax-mulcom 8025

This theorem is referenced by:  adddir  8062  mullid  8069  mulcomi  8077  mulcomd  8093  mul12  8200  mul32  8201  mul31  8202  muladd  8455  subdir  8457  mul01  8460  mulneg2  8467  recextlem1  8723  divmulap3  8749  div23ap  8763  div13ap  8765  div12ap  8766  divmulasscomap  8768  divcanap4  8771  divmul13ap  8787  divmul24ap  8788  divcanap7  8793  div2negap  8807  prodgt02  8925  prodge02  8927  ltmul2  8928  lemul2  8929  lemul2a  8931  ltmulgt12  8937  lemulge12  8939  ltmuldiv2  8947  ltdivmul2  8950  ledivmul2  8952  lemuldiv2  8954  times2  9164  modqcyc2  10503  subsq  10789  cjmulrcl  11169  imval2  11176  abscj  11334  sqabsadd  11337  sqabssub  11338  prod3fmul  11823  prodmodclem3  11857  efcllemp  11940  efexp  11964  sinmul  12026  demoivreALT  12056  dvdsmul1  12095  odd2np1lem  12154  odd2np1  12155  opeo  12179  omeo  12180  modgcd  12283  dvdsgcd  12304  gcdmultiple  12312  coprmdvds  12385  coprmdvds2  12386  qredeq  12389  modprm0  12548  modprmn0modprm0  12550  coprimeprodsq2  12552  cncrng  14302  cnfldui  14322  ef2kpi  15249  sinperlem  15251  sinmpi  15258  cosmpi  15259  sinppi  15260  cosppi  15261  cxpcom  15381  perfectlem1  15442  perfectlem2  15443  perfect  15444  lgsdir2lem4  15479  lgsdir2  15481  lgsquadlem2  15526  lgsquad2  15531