Theorem mulcom 10022

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483   ∈ wcel 1990  (class class class)co 6650  ℂcc 9934   · cmul 9941

This theorem was proved from axioms:  ax-mulcom 10000

This theorem is referenced by:  adddir  10031  mulid2  10038  mulcomi  10046  mulcomd  10061  mul12  10202  mul32  10203  mul31  10204  mul01  10215  muladd  10462  subdir  10464  mulneg2  10467  recextlem1  10657  mulcan2g  10681  divmul3  10690  div23  10704  div13  10706  div12  10707  divmulasscom  10709  divcan4  10712  divmul13  10728  divmul24  10729  divcan7  10734  div2neg  10748  prodgt02  10869  prodge02  10871  ltmul2  10874  lemul2  10876  lemul2a  10878  ltmulgt12  10884  lemulge12  10886  ltmuldiv2  10897  ltdivmul2  10900  lt2mul2div  10901  ledivmul2  10902  lemuldiv2  10904  supmul  10995  times2  11146  modcyc  12705  modcyc2  12706  modmulmodr  12736  subsq  12972  cjmulrcl  13884  imval2  13891  abscj  14019  sqabsadd  14022  sqabssub  14023  sqreulem  14099  iseraltlem2  14413  iseraltlem3  14414  climcndslem2  14582  prodfmul  14622  prodmolem3  14663  bpoly3  14789  efcllem  14808  efexp  14831  sinmul  14902  demoivreALT  14931  dvdsmul1  15003  odd2np1lem  15064  odd2np1  15065  opeo  15089  omeo  15090  modgcd  15253  bezoutlem1  15256  dvdsgcd  15261  gcdmultiple  15269  coprmdvds  15366  coprmdvdsOLD  15367  coprmdvds2  15368  qredeq  15371  eulerthlem2  15487  modprm0  15510  modprmn0modprm0  15512  coprimeprodsq2  15514  prmreclem6  15625  odmod  17965  cncrng  19767  cnsrng  19780  pcoass  22824  clmvscom  22890  dvlipcn  23757  plydivlem4  24051  quotcan  24064  aaliou3lem3  24099  ef2kpi  24230  sinperlem  24232  sinmpi  24239  cosmpi  24240  sinppi  24241  cosppi  24242  sineq0  24273  tanregt0  24285  logneg  24334  lognegb  24336  logimul  24360  tanarg  24365  logtayl  24406  cxpsqrtlem  24448  cubic2  24575  quart1  24583  log2cnv  24671  basellem1  24807  basellem3  24809  basellem5  24811  basellem8  24814  mumul  24907  chtublem  24936  perfectlem1  24954  perfectlem2  24955  perfect  24956  dchrabl  24979  bposlem6  25014  bposlem9  25017  lgsdir2lem4  25053  lgsdir2  25055  lgsdir  25057  lgsdi  25059  lgsquadlem2  25106  lgsquad2  25111  rpvmasum2  25201  mulog2sumlem1  25223  pntibndlem2  25280  pntibndlem3  25281  pntlemf  25294  nvscom  27484  ipasslem11  27695  ipblnfi  27711  hvmulcom  27900  h1de2bi  28413  homul12  28664  riesz3i  28921  riesz1  28924  kbass4  28978  sin2h  33399  heiborlem6  33615  rmym1  37500  expgrowthi  38532  expgrowth  38534  stoweidlem10  40227  perfectALTVlem1  41630  perfectALTVlem2  41631  perfectALTV  41632  tgoldbachlt  41704  tgoldbachltOLD  41710  2zrngnmlid2  41951