Theorem mulcom 11215

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  (class class class)co 7405  ℂcc 11127   · cmul 11134

This theorem was proved from axioms:  ax-mulcom 11193

This theorem is referenced by:  adddir  11226  mullid  11234  mulcomi  11243  mulcomd  11256  mul12  11400  mul32  11401  mul31  11402  mul4r  11404  mul01  11414  muladd  11669  subdir  11671  mulneg2  11674  recextlem1  11867  mulcan2g  11891  divmul3  11901  div23  11915  div13  11917  div12  11918  divmulasscom  11920  divcan4  11923  divmul13  11944  divmul24  11945  divcan7  11950  div2neg  11964  prodgt02  12089  ltmul2  12092  lemul2  12094  lemul2a  12096  ltmulgt12  12102  lemulge12  12105  ltmuldiv2  12116  ltdivmul2  12119  lt2mul2div  12120  ledivmul2  12121  lemuldiv2  12123  supmul  12214  times2  12377  modcyc  13923  modcyc2  13924  modmulmodr  13955  subsq  14228  cjmulrcl  15163  imval2  15170  abscj  15298  sqabsadd  15301  sqabssub  15302  sqreulem  15378  iseraltlem2  15699  iseraltlem3  15700  climcndslem2  15866  prodfmul  15906  prodmolem3  15949  bpoly3  16074  efcllem  16093  efexp  16119  sinmul  16190  demoivreALT  16219  dvdsmul1  16297  odd2np1lem  16359  odd2np1  16360  opeo  16384  omeo  16385  modgcd  16551  bezoutlem1  16558  dvdsgcd  16563  coprmdvds  16672  coprmdvds2  16673  qredeq  16676  eulerthlem2  16801  modprm0  16825  modprmn0modprm0  16827  coprimeprodsq2  16829  prmreclem6  16941  odmod  19527  cncrng  21351  cncrngOLD  21352  cnsrng  21368  pcoass  24975  clmvscom  25041  dvlipcn  25951  plydivlem4  26256  quotcan  26269  aaliou3lem3  26304  ef2kpi  26439  sinperlem  26441  sinmpi  26448  cosmpi  26449  sinppi  26450  cosppi  26451  sineq0  26485  tanregt0  26500  logneg  26549  lognegb  26551  logimul  26575  tanarg  26580  logtayl  26621  cxpsqrtlem  26663  cxpcom  26700  cubic2  26810  quart1  26818  log2cnv  26906  basellem1  27043  basellem3  27045  basellem5  27047  basellem8  27050  mumul  27143  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  30610  ipasslem11  30821  ipblnfi  30836  hvmulcom  31024  h1de2bi  31535  homul12  31786  riesz3i  32043  riesz1  32046  kbass4  32100  sin2h  37634  heiborlem6  37840  rmym1  42959  expgrowthi  44357  expgrowth  44359  stoweidlem10  46039  perfectALTVlem1  47735  perfectALTVlem2  47736  perfectALTV  47737  tgoldbachlt  47830  2zrngnmlid2  48232