Theorem mulcom 11099

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  (class class class)co 7352  ℂcc 11011   · cmul 11018

This theorem was proved from axioms:  ax-mulcom 11077

This theorem is referenced by:  adddir  11110  mullid  11118  mulcomi  11127  mulcomd  11140  mul12  11285  mul32  11286  mul31  11287  mul4r  11289  mul01  11299  muladd  11556  subdir  11558  mulneg2  11561  recextlem1  11754  mulcan2g  11778  divmul3  11788  div23  11802  div13  11804  div12  11805  divmulasscom  11807  divcan4  11810  divmul13  11831  divmul24  11832  divcan7  11837  div2neg  11851  prodgt02  11976  ltmul2  11979  lemul2  11981  lemul2a  11983  ltmulgt12  11989  lemulge12  11992  ltmuldiv2  12003  ltdivmul2  12006  lt2mul2div  12007  ledivmul2  12008  lemuldiv2  12010  supmul  12101  times2  12264  modcyc  13812  modcyc2  13813  modmulmodr  13846  subsq  14119  cjmulrcl  15053  imval2  15060  abscj  15188  sqabsadd  15191  sqabssub  15192  sqreulem  15269  iseraltlem2  15592  iseraltlem3  15593  climcndslem2  15759  prodfmul  15799  prodmolem3  15842  bpoly3  15967  efcllem  15986  efexp  16012  sinmul  16083  demoivreALT  16112  dvdsmul1  16190  odd2np1lem  16253  odd2np1  16254  opeo  16278  omeo  16279  modgcd  16445  bezoutlem1  16452  dvdsgcd  16457  coprmdvds  16566  coprmdvds2  16567  qredeq  16570  eulerthlem2  16695  modprm0  16719  modprmn0modprm0  16721  coprimeprodsq2  16723  prmreclem6  16835  odmod  19460  cncrng  21327  cncrngOLD  21328  cnsrng  21344  pcoass  24952  clmvscom  25018  dvlipcn  25927  plydivlem4  26232  quotcan  26245  aaliou3lem3  26280  ef2kpi  26415  sinperlem  26417  sinmpi  26424  cosmpi  26425  sinppi  26426  cosppi  26427  sineq0  26461  tanregt0  26476  logneg  26525  lognegb  26527  logimul  26551  tanarg  26556  logtayl  26597  cxpsqrtlem  26639  cxpcom  26676  cubic2  26786  quart1  26794  log2cnv  26882  basellem1  27019  basellem3  27021  basellem5  27023  basellem8  27026  mumul  27119  chtublem  27150  perfectlem1  27168  perfectlem2  27169  perfect  27170  dchrabl  27193  bposlem6  27228  bposlem9  27231  lgsdir2lem4  27267  lgsdir2  27269  lgsquadlem2  27320  lgsquad2  27325  rpvmasum2  27451  mulog2sumlem1  27473  pntibndlem2  27530  pntibndlem3  27531  pntlemf  27544  nvscom  30611  ipasslem11  30822  ipblnfi  30837  hvmulcom  31025  h1de2bi  31536  homul12  31787  riesz3i  32044  riesz1  32047  kbass4  32101  sin2h  37670  heiborlem6  37876  rmym1  43052  expgrowthi  44450  expgrowth  44452  stoweidlem10  46132  perfectALTVlem1  47845  perfectALTVlem2  47846  perfectALTV  47847  tgoldbachlt  47940  2zrngnmlid2  48381