Theorem mulcom 11122

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034   · cmul 11041

This theorem was proved from axioms:  ax-mulcom 11100

This theorem is referenced by:  adddir  11133  mullid  11141  mulcomi  11151  mulcomd  11164  mul12  11309  mul32  11310  mul31  11311  mul4r  11313  mul01  11323  muladd  11580  subdir  11582  mulneg2  11585  recextlem1  11778  mulcan2g  11802  divmul3  11812  div23  11826  div13  11828  div12  11829  divmulasscom  11831  divcan4  11834  divmul13  11856  divmul24  11857  divcan7  11862  div2neg  11876  prodgt02  12001  ltmul2  12004  lemul2  12006  lemul2a  12008  ltmulgt12  12014  lemulge12  12017  ltmuldiv2  12028  ltdivmul2  12031  lt2mul2div  12032  ledivmul2  12033  lemuldiv2  12035  supmul  12126  times2  12311  modcyc  13863  modcyc2  13864  modmulmodr  13897  subsq  14170  cjmulrcl  15104  imval2  15111  abscj  15239  sqabsadd  15242  sqabssub  15243  sqreulem  15320  iseraltlem2  15643  iseraltlem3  15644  climcndslem2  15813  prodfmul  15853  prodmolem3  15896  bpoly3  16021  efcllem  16040  efexp  16066  sinmul  16137  demoivreALT  16166  dvdsmul1  16244  odd2np1lem  16307  odd2np1  16308  opeo  16332  omeo  16333  modgcd  16499  bezoutlem1  16506  dvdsgcd  16511  coprmdvds  16620  coprmdvds2  16621  qredeq  16624  eulerthlem2  16750  modprm0  16774  modprmn0modprm0  16776  coprimeprodsq2  16778  prmreclem6  16890  odmod  19519  cncrng  21375  cnsrng  21388  pcoass  25016  clmvscom  25082  dvlipcn  25986  plydivlem4  26287  quotcan  26300  aaliou3lem3  26335  ef2kpi  26467  sinperlem  26469  sinmpi  26476  cosmpi  26477  sinppi  26478  cosppi  26479  sineq0  26513  tanregt0  26528  logneg  26577  lognegb  26579  logimul  26603  tanarg  26608  logtayl  26649  cxpsqrtlem  26691  cxpcom  26728  cubic2  26837  quart1  26845  log2cnv  26933  basellem1  27069  basellem3  27071  basellem5  27073  basellem8  27076  mumul  27169  chtublem  27199  perfectlem1  27217  perfectlem2  27218  perfect  27219  dchrabl  27242  bposlem6  27277  bposlem9  27280  lgsdir2lem4  27316  lgsdir2  27318  lgsquadlem2  27369  lgsquad2  27374  rpvmasum2  27500  mulog2sumlem1  27522  pntibndlem2  27579  pntibndlem3  27580  pntlemf  27593  nvscom  30725  ipasslem11  30936  ipblnfi  30951  hvmulcom  31139  h1de2bi  31650  homul12  31901  riesz3i  32158  riesz1  32161  kbass4  32215  sin2h  37984  heiborlem6  38190  rmym1  43387  expgrowthi  44784  expgrowth  44786  stoweidlem10  46460  perfectALTVlem1  48219  perfectALTVlem2  48220  perfectALTV  48221  tgoldbachlt  48314  2zrngnmlid2  48755