Theorem mulcom 11156

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141  (class class class)co 7392  ℂcc 11068   · cmul 11075

This theorem was proved from axioms:  ax-mulcom 11134

This theorem is referenced by:  adddir  11167  mullid  11177  mulcomi  11187  mulcomd  11200  mul12  11345  mul32  11346  mul31  11347  mul4r  11349  mul01  11359  muladd  11616  subdir  11618  mulneg2  11621  recextlem1  11814  mulcan2g  11838  divmul3  11847  div23  11861  div13  11863  div12  11864  divmulasscom  11866  divcan4  11869  divmul13  11891  divmul24  11892  divcan7  11897  div2neg  11911  prodgt02  12036  ltmul2  12039  lemul2  12041  lemul2a  12043  ltmulgt12  12049  lemulge12  12052  ltmuldiv2  12063  ltdivmul2  12066  lt2mul2div  12067  ledivmul2  12068  lemuldiv2  12070  supmul  12161  times2  12351  modcyc  13913  modcyc2  13914  modmulmodr  13947  subsq  14220  cjmulrcl  15154  imval2  15161  abscj  15289  sqabsadd  15292  sqabssub  15293  sqreulem  15370  iseraltlem2  15693  iseraltlem3  15694  climcndslem2  15863  prodfmul  15903  prodmolem3  15946  bpoly3  16071  efcllem  16090  efexp  16116  sinmul  16187  demoivreALT  16216  dvdsmul1  16294  odd2np1lem  16357  odd2np1  16358  opeo  16382  omeo  16383  modgcd  16549  bezoutlem1  16556  dvdsgcd  16561  coprmdvds  16670  coprmdvds2  16671  qredeq  16674  eulerthlem2  16800  modprm0  16824  modprmn0modprm0  16826  coprimeprodsq2  16828  prmreclem6  16940  odmod  19569  cncrng  21425  cnsrng  21438  pcoass  25066  clmvscom  25132  dvlipcn  26036  plydivlem4  26337  quotcan  26350  aaliou3lem3  26385  ef2kpi  26520  sinperlem  26522  sinmpi  26529  cosmpi  26530  sinppi  26531  cosppi  26532  sineq0  26566  tanregt0  26581  logneg  26630  lognegb  26632  logimul  26656  tanarg  26661  logtayl  26702  cxpsqrtlem  26744  cxpcom  26781  cubic2  26890  quart1  26898  log2cnv  26986  basellem1  27122  basellem3  27124  basellem5  27126  basellem8  27129  mumul  27222  chtublem  27252  perfectlem1  27270  perfectlem2  27271  perfect  27272  dchrabl  27295  bposlem6  27330  bposlem9  27333  lgsdir2lem4  27369  lgsdir2  27371  lgsquadlem2  27422  lgsquad2  27427  rpvmasum2  27553  mulog2sumlem1  27575  pntibndlem2  27632  pntibndlem3  27633  pntlemf  27646  nvscom  30778  ipasslem11  30989  ipblnfi  31004  hvmulcom  31192  h1de2bi  31703  homul12  31954  riesz3i  32211  riesz1  32214  kbass4  32268  sin2h  38073  heiborlem6  38279  rmym1  43476  expgrowthi  44873  expgrowth  44875  stoweidlem10  46548  perfectALTVlem1  48307  perfectALTVlem2  48308  perfectALTV  48309  tgoldbachlt  48402  2zrngnmlid2  48843