Theorem mulcom 11115

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027   · cmul 11034

This theorem was proved from axioms:  ax-mulcom 11093

This theorem is referenced by:  adddir  11126  mullid  11134  mulcomi  11144  mulcomd  11157  mul12  11302  mul32  11303  mul31  11304  mul4r  11306  mul01  11316  muladd  11573  subdir  11575  mulneg2  11578  recextlem1  11771  mulcan2g  11795  divmul3  11805  div23  11819  div13  11821  div12  11822  divmulasscom  11824  divcan4  11827  divmul13  11849  divmul24  11850  divcan7  11855  div2neg  11869  prodgt02  11994  ltmul2  11997  lemul2  11999  lemul2a  12001  ltmulgt12  12007  lemulge12  12010  ltmuldiv2  12021  ltdivmul2  12024  lt2mul2div  12025  ledivmul2  12026  lemuldiv2  12028  supmul  12119  times2  12304  modcyc  13856  modcyc2  13857  modmulmodr  13890  subsq  14163  cjmulrcl  15097  imval2  15104  abscj  15232  sqabsadd  15235  sqabssub  15236  sqreulem  15313  iseraltlem2  15636  iseraltlem3  15637  climcndslem2  15806  prodfmul  15846  prodmolem3  15889  bpoly3  16014  efcllem  16033  efexp  16059  sinmul  16130  demoivreALT  16159  dvdsmul1  16237  odd2np1lem  16300  odd2np1  16301  opeo  16325  omeo  16326  modgcd  16492  bezoutlem1  16499  dvdsgcd  16504  coprmdvds  16613  coprmdvds2  16614  qredeq  16617  eulerthlem2  16743  modprm0  16767  modprmn0modprm0  16769  coprimeprodsq2  16771  prmreclem6  16883  odmod  19512  cncrng  21378  cncrngOLD  21379  cnsrng  21395  pcoass  25001  clmvscom  25067  dvlipcn  25971  plydivlem4  26273  quotcan  26286  aaliou3lem3  26321  ef2kpi  26455  sinperlem  26457  sinmpi  26464  cosmpi  26465  sinppi  26466  cosppi  26467  sineq0  26501  tanregt0  26516  logneg  26565  lognegb  26567  logimul  26591  tanarg  26596  logtayl  26637  cxpsqrtlem  26679  cxpcom  26716  cubic2  26825  quart1  26833  log2cnv  26921  basellem1  27058  basellem3  27060  basellem5  27062  basellem8  27065  mumul  27158  chtublem  27188  perfectlem1  27206  perfectlem2  27207  perfect  27208  dchrabl  27231  bposlem6  27266  bposlem9  27269  lgsdir2lem4  27305  lgsdir2  27307  lgsquadlem2  27358  lgsquad2  27363  rpvmasum2  27489  mulog2sumlem1  27511  pntibndlem2  27568  pntibndlem3  27569  pntlemf  27582  nvscom  30715  ipasslem11  30926  ipblnfi  30941  hvmulcom  31129  h1de2bi  31640  homul12  31891  riesz3i  32148  riesz1  32151  kbass4  32205  sin2h  37945  heiborlem6  38151  rmym1  43381  expgrowthi  44778  expgrowth  44780  stoweidlem10  46456  perfectALTVlem1  48209  perfectALTVlem2  48210  perfectALTV  48211  tgoldbachlt  48304  2zrngnmlid2  48745