Theorem mulcom 11124

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036   · cmul 11043

This theorem was proved from axioms:  ax-mulcom 11102

This theorem is referenced by:  adddir  11135  mullid  11143  mulcomi  11152  mulcomd  11165  mul12  11310  mul32  11311  mul31  11312  mul4r  11314  mul01  11324  muladd  11581  subdir  11583  mulneg2  11586  recextlem1  11779  mulcan2g  11803  divmul3  11813  div23  11827  div13  11829  div12  11830  divmulasscom  11832  divcan4  11835  divmul13  11856  divmul24  11857  divcan7  11862  div2neg  11876  prodgt02  12001  ltmul2  12004  lemul2  12006  lemul2a  12008  ltmulgt12  12014  lemulge12  12017  ltmuldiv2  12028  ltdivmul2  12031  lt2mul2div  12032  ledivmul2  12033  lemuldiv2  12035  supmul  12126  times2  12289  modcyc  13838  modcyc2  13839  modmulmodr  13872  subsq  14145  cjmulrcl  15079  imval2  15086  abscj  15214  sqabsadd  15217  sqabssub  15218  sqreulem  15295  iseraltlem2  15618  iseraltlem3  15619  climcndslem2  15785  prodfmul  15825  prodmolem3  15868  bpoly3  15993  efcllem  16012  efexp  16038  sinmul  16109  demoivreALT  16138  dvdsmul1  16216  odd2np1lem  16279  odd2np1  16280  opeo  16304  omeo  16305  modgcd  16471  bezoutlem1  16478  dvdsgcd  16483  coprmdvds  16592  coprmdvds2  16593  qredeq  16596  eulerthlem2  16721  modprm0  16745  modprmn0modprm0  16747  coprimeprodsq2  16749  prmreclem6  16861  odmod  19487  cncrng  21355  cncrngOLD  21356  cnsrng  21372  pcoass  24992  clmvscom  25058  dvlipcn  25967  plydivlem4  26272  quotcan  26285  aaliou3lem3  26320  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  26826  quart1  26834  log2cnv  26922  basellem1  27059  basellem3  27061  basellem5  27063  basellem8  27066  mumul  27159  chtublem  27190  perfectlem1  27208  perfectlem2  27209  perfect  27210  dchrabl  27233  bposlem6  27268  bposlem9  27271  lgsdir2lem4  27307  lgsdir2  27309  lgsquadlem2  27360  lgsquad2  27365  rpvmasum2  27491  mulog2sumlem1  27513  pntibndlem2  27570  pntibndlem3  27571  pntlemf  27584  nvscom  30716  ipasslem11  30927  ipblnfi  30942  hvmulcom  31130  h1de2bi  31641  homul12  31892  riesz3i  32149  riesz1  32152  kbass4  32206  sin2h  37855  heiborlem6  38061  rmym1  43286  expgrowthi  44683  expgrowth  44685  stoweidlem10  46362  perfectALTVlem1  48075  perfectALTVlem2  48076  perfectALTV  48077  tgoldbachlt  48170  2zrngnmlid2  48611