Theorem mulcom 10888

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

Assertion

Ref	Expression
mulcom	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))

Proof of Theorem mulcom

Step	Hyp	Ref	Expression
1		ax-mulcom 10866	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800   · cmul 10807

This theorem was proved from axioms:  ax-mulcom 10866

This theorem is referenced by:  adddir  10897  mulid2  10905  mulcomi  10914  mulcomd  10927  mul12  11070  mul32  11071  mul31  11072  mul4r  11074  mul01  11084  muladd  11337  subdir  11339  mulneg2  11342  recextlem1  11535  mulcan2g  11559  divmul3  11568  div23  11582  div13  11584  div12  11585  divmulasscom  11587  divcan4  11590  divmul13  11608  divmul24  11609  divcan7  11614  div2neg  11628  prodgt02  11753  ltmul2  11756  lemul2  11758  lemul2a  11760  ltmulgt12  11766  lemulge12  11768  ltmuldiv2  11779  ltdivmul2  11782  lt2mul2div  11783  ledivmul2  11784  lemuldiv2  11786  supmul  11877  times2  12040  modcyc  13554  modcyc2  13555  modmulmodr  13585  subsq  13854  cjmulrcl  14783  imval2  14790  abscj  14919  sqabsadd  14922  sqabssub  14923  sqreulem  14999  iseraltlem2  15322  iseraltlem3  15323  climcndslem2  15490  prodfmul  15530  prodmolem3  15571  bpoly3  15696  efcllem  15715  efexp  15738  sinmul  15809  demoivreALT  15838  dvdsmul1  15915  odd2np1lem  15977  odd2np1  15978  opeo  16002  omeo  16003  modgcd  16168  bezoutlem1  16175  dvdsgcd  16180  gcdmultipleOLD  16188  coprmdvds  16286  coprmdvds2  16287  qredeq  16290  eulerthlem2  16411  modprm0  16434  modprmn0modprm0  16436  coprimeprodsq2  16438  prmreclem6  16550  odmod  19069  cncrng  20531  cnsrng  20544  pcoass  24093  clmvscom  24159  dvlipcn  25063  plydivlem4  25361  quotcan  25374  aaliou3lem3  25409  ef2kpi  25540  sinperlem  25542  sinmpi  25549  cosmpi  25550  sinppi  25551  cosppi  25552  sineq0  25585  tanregt0  25600  logneg  25648  lognegb  25650  logimul  25674  tanarg  25679  logtayl  25720  cxpsqrtlem  25762  cxpcom  25797  cubic2  25903  quart1  25911  log2cnv  25999  basellem1  26135  basellem3  26137  basellem5  26139  basellem8  26142  mumul  26235  chtublem  26264  perfectlem1  26282  perfectlem2  26283  perfect  26284  dchrabl  26307  bposlem6  26342  bposlem9  26345  lgsdir2lem4  26381  lgsdir2  26383  lgsquadlem2  26434  lgsquad2  26439  rpvmasum2  26565  mulog2sumlem1  26587  pntibndlem2  26644  pntibndlem3  26645  pntlemf  26658  nvscom  28892  ipasslem11  29103  ipblnfi  29118  hvmulcom  29306  h1de2bi  29817  homul12  30068  riesz3i  30325  riesz1  30328  kbass4  30382  sin2h  35694  heiborlem6  35901  rmym1  40673  expgrowthi  41840  expgrowth  41842  stoweidlem10  43441  perfectALTVlem1  45061  perfectALTVlem2  45062  perfectALTV  45063  tgoldbachlt  45156  2zrngnmlid2  45397