Theorem mulcom 11124

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036   · cmul 11043

This theorem was proved from axioms:  ax-mulcom 11102

This theorem is referenced by:  adddir  11135  mullid  11143  mulcomi  11153  mulcomd  11166  mul12  11311  mul32  11312  mul31  11313  mul4r  11315  mul01  11325  muladd  11582  subdir  11584  mulneg2  11587  recextlem1  11780  mulcan2g  11804  divmul3  11814  div23  11828  div13  11830  div12  11831  divmulasscom  11833  divcan4  11836  divmul13  11858  divmul24  11859  divcan7  11864  div2neg  11878  prodgt02  12003  ltmul2  12006  lemul2  12008  lemul2a  12010  ltmulgt12  12016  lemulge12  12019  ltmuldiv2  12030  ltdivmul2  12033  lt2mul2div  12034  ledivmul2  12035  lemuldiv2  12037  supmul  12128  times2  12313  modcyc  13865  modcyc2  13866  modmulmodr  13899  subsq  14172  cjmulrcl  15106  imval2  15113  abscj  15241  sqabsadd  15244  sqabssub  15245  sqreulem  15322  iseraltlem2  15645  iseraltlem3  15646  climcndslem2  15815  prodfmul  15855  prodmolem3  15898  bpoly3  16023  efcllem  16042  efexp  16068  sinmul  16139  demoivreALT  16168  dvdsmul1  16246  odd2np1lem  16309  odd2np1  16310  opeo  16334  omeo  16335  modgcd  16501  bezoutlem1  16508  dvdsgcd  16513  coprmdvds  16622  coprmdvds2  16623  qredeq  16626  eulerthlem2  16752  modprm0  16776  modprmn0modprm0  16778  coprimeprodsq2  16780  prmreclem6  16892  odmod  19521  cncrng  21373  cnsrng  21386  pcoass  24991  clmvscom  25057  dvlipcn  25961  plydivlem4  26262  quotcan  26275  aaliou3lem3  26310  ef2kpi  26442  sinperlem  26444  sinmpi  26451  cosmpi  26452  sinppi  26453  cosppi  26454  sineq0  26488  tanregt0  26503  logneg  26552  lognegb  26554  logimul  26578  tanarg  26583  logtayl  26624  cxpsqrtlem  26666  cxpcom  26703  cubic2  26812  quart1  26820  log2cnv  26908  basellem1  27044  basellem3  27046  basellem5  27048  basellem8  27051  mumul  27144  chtublem  27174  perfectlem1  27192  perfectlem2  27193  perfect  27194  dchrabl  27217  bposlem6  27252  bposlem9  27255  lgsdir2lem4  27291  lgsdir2  27293  lgsquadlem2  27344  lgsquad2  27349  rpvmasum2  27475  mulog2sumlem1  27497  pntibndlem2  27554  pntibndlem3  27555  pntlemf  27568  nvscom  30700  ipasslem11  30911  ipblnfi  30926  hvmulcom  31114  h1de2bi  31625  homul12  31876  riesz3i  32133  riesz1  32136  kbass4  32190  sin2h  37931  heiborlem6  38137  rmym1  43363  expgrowthi  44760  expgrowth  44762  stoweidlem10  46438  perfectALTVlem1  48197  perfectALTVlem2  48198  perfectALTV  48199  tgoldbachlt  48292  2zrngnmlid2  48733