Theorem mulcom 10815

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2110  (class class class)co 7213  ℂcc 10727   · cmul 10734

This theorem was proved from axioms:  ax-mulcom 10793

This theorem is referenced by:  adddir  10824  mulid2  10832  mulcomi  10841  mulcomd  10854  mul12  10997  mul32  10998  mul31  10999  mul4r  11001  mul01  11011  muladd  11264  subdir  11266  mulneg2  11269  recextlem1  11462  mulcan2g  11486  divmul3  11495  div23  11509  div13  11511  div12  11512  divmulasscom  11514  divcan4  11517  divmul13  11535  divmul24  11536  divcan7  11541  div2neg  11555  prodgt02  11680  ltmul2  11683  lemul2  11685  lemul2a  11687  ltmulgt12  11693  lemulge12  11695  ltmuldiv2  11706  ltdivmul2  11709  lt2mul2div  11710  ledivmul2  11711  lemuldiv2  11713  supmul  11804  times2  11967  modcyc  13479  modcyc2  13480  modmulmodr  13510  subsq  13778  cjmulrcl  14707  imval2  14714  abscj  14843  sqabsadd  14846  sqabssub  14847  sqreulem  14923  iseraltlem2  15246  iseraltlem3  15247  climcndslem2  15414  prodfmul  15454  prodmolem3  15495  bpoly3  15620  efcllem  15639  efexp  15662  sinmul  15733  demoivreALT  15762  dvdsmul1  15839  odd2np1lem  15901  odd2np1  15902  opeo  15926  omeo  15927  modgcd  16092  bezoutlem1  16099  dvdsgcd  16104  gcdmultipleOLD  16112  coprmdvds  16210  coprmdvds2  16211  qredeq  16214  eulerthlem2  16335  modprm0  16358  modprmn0modprm0  16360  coprimeprodsq2  16362  prmreclem6  16474  odmod  18938  cncrng  20384  cnsrng  20397  pcoass  23921  clmvscom  23987  dvlipcn  24891  plydivlem4  25189  quotcan  25202  aaliou3lem3  25237  ef2kpi  25368  sinperlem  25370  sinmpi  25377  cosmpi  25378  sinppi  25379  cosppi  25380  sineq0  25413  tanregt0  25428  logneg  25476  lognegb  25478  logimul  25502  tanarg  25507  logtayl  25548  cxpsqrtlem  25590  cxpcom  25625  cubic2  25731  quart1  25739  log2cnv  25827  basellem1  25963  basellem3  25965  basellem5  25967  basellem8  25970  mumul  26063  chtublem  26092  perfectlem1  26110  perfectlem2  26111  perfect  26112  dchrabl  26135  bposlem6  26170  bposlem9  26173  lgsdir2lem4  26209  lgsdir2  26211  lgsquadlem2  26262  lgsquad2  26267  rpvmasum2  26393  mulog2sumlem1  26415  pntibndlem2  26472  pntibndlem3  26473  pntlemf  26486  nvscom  28710  ipasslem11  28921  ipblnfi  28936  hvmulcom  29124  h1de2bi  29635  homul12  29886  riesz3i  30143  riesz1  30146  kbass4  30200  sin2h  35504  heiborlem6  35711  rmym1  40460  expgrowthi  41624  expgrowth  41626  stoweidlem10  43226  perfectALTVlem1  44846  perfectALTVlem2  44847  perfectALTV  44848  tgoldbachlt  44941  2zrngnmlid2  45182