Theorem mulcom 11174

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086   · cmul 11093

This theorem was proved from axioms:  ax-mulcom 11152

This theorem is referenced by:  adddir  11185  mullid  11195  mulcomi  11205  mulcomd  11218  mul12  11363  mul32  11364  mul31  11365  mul4r  11367  mul01  11377  muladd  11634  subdir  11636  mulneg2  11639  recextlem1  11832  mulcan2g  11856  divmul3  11865  div23  11879  div13  11881  div12  11882  divmulasscom  11884  divcan4  11887  divmul13  11909  divmul24  11910  divcan7  11915  div2neg  11929  prodgt02  12054  ltmul2  12057  lemul2  12059  lemul2a  12061  ltmulgt12  12066  lemulge12  12069  ltmuldiv2  12080  ltdivmul2  12083  lt2mul2div  12084  ledivmul2  12085  lemuldiv2  12087  supmul  12178  times2  12368  modcyc  13930  modcyc2  13931  modmulmodr  13964  subsq  14237  cjmulrcl  15185  imval2  15192  abscj  15320  sqabsadd  15323  sqabssub  15324  sqreulem  15401  iseraltlem2  15724  iseraltlem3  15725  climcndslem2  15894  prodfmul  15934  prodmolem3  15977  bpoly3  16102  efcllem  16121  efexp  16147  sinmul  16218  demoivreALT  16247  dvdsmul1  16325  odd2np1lem  16388  odd2np1  16389  opeo  16413  omeo  16414  modgcd  16580  bezoutlem1  16587  dvdsgcd  16592  coprmdvds  16701  coprmdvds2  16702  qredeq  16705  eulerthlem2  16831  modprm0  16855  modprmn0modprm0  16857  coprimeprodsq2  16859  prmreclem6  16971  odmod  19607  cncrng  21503  cnsrng  21516  pcoass  25144  clmvscom  25210  dvlipcn  26114  plydivlem4  26418  quotcan  26431  aaliou3lem3  26466  ef2kpi  26601  sinperlem  26603  sinmpi  26610  cosmpi  26611  sinppi  26612  cosppi  26613  sineq0  26647  tanregt0  26662  logneg  26711  lognegb  26713  logimul  26737  tanarg  26742  logtayl  26783  cxpsqrtlem  26825  cxpcom  26862  cubic2  26971  quart1  26979  log2cnv  27067  basellem1  27203  basellem3  27205  basellem5  27207  basellem8  27210  mumul  27303  chtublem  27333  perfectlem1  27351  perfectlem2  27352  perfect  27353  dchrabl  27376  bposlem6  27411  bposlem9  27414  lgsdir2lem4  27450  lgsdir2  27452  lgsquadlem2  27503  lgsquad2  27508  rpvmasum2  27634  mulog2sumlem1  27656  pntibndlem2  27713  pntibndlem3  27714  pntlemf  27727  nvscom  30890  ipasslem11  31101  ipblnfi  31116  hvmulcom  31304  h1de2bi  31815  homul12  32066  riesz3i  32323  riesz1  32326  kbass4  32380  sin2h  38121  heiborlem6  38327  rmym1  43524  expgrowthi  44907  expgrowth  44909  stoweidlem10  46582  perfectALTVlem1  48341  perfectALTVlem2  48342  perfectALTV  48343  tgoldbachlt  48436  2zrngnmlid2  48877