Theorem mulcom 11027

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1540   ∈ wcel 2105  (class class class)co 7313  ℂcc 10939   · cmul 10946

This theorem was proved from axioms:  ax-mulcom 11005

This theorem is referenced by:  adddir  11036  mulid2  11044  mulcomi  11053  mulcomd  11066  mul12  11210  mul32  11211  mul31  11212  mul4r  11214  mul01  11224  muladd  11477  subdir  11479  mulneg2  11482  recextlem1  11675  mulcan2g  11699  divmul3  11708  div23  11722  div13  11724  div12  11725  divmulasscom  11727  divcan4  11730  divmul13  11748  divmul24  11749  divcan7  11754  div2neg  11768  prodgt02  11893  ltmul2  11896  lemul2  11898  lemul2a  11900  ltmulgt12  11906  lemulge12  11908  ltmuldiv2  11919  ltdivmul2  11922  lt2mul2div  11923  ledivmul2  11924  lemuldiv2  11926  supmul  12017  times2  12180  modcyc  13696  modcyc2  13697  modmulmodr  13727  subsq  13996  cjmulrcl  14924  imval2  14931  abscj  15060  sqabsadd  15063  sqabssub  15064  sqreulem  15140  iseraltlem2  15463  iseraltlem3  15464  climcndslem2  15631  prodfmul  15671  prodmolem3  15712  bpoly3  15837  efcllem  15856  efexp  15879  sinmul  15950  demoivreALT  15979  dvdsmul1  16056  odd2np1lem  16118  odd2np1  16119  opeo  16143  omeo  16144  modgcd  16309  bezoutlem1  16316  dvdsgcd  16321  coprmdvds  16425  coprmdvds2  16426  qredeq  16429  eulerthlem2  16550  modprm0  16573  modprmn0modprm0  16575  coprimeprodsq2  16577  prmreclem6  16689  odmod  19221  cncrng  20690  cnsrng  20703  pcoass  24258  clmvscom  24324  dvlipcn  25229  plydivlem4  25527  quotcan  25540  aaliou3lem3  25575  ef2kpi  25706  sinperlem  25708  sinmpi  25715  cosmpi  25716  sinppi  25717  cosppi  25718  sineq0  25751  tanregt0  25766  logneg  25814  lognegb  25816  logimul  25840  tanarg  25845  logtayl  25886  cxpsqrtlem  25928  cxpcom  25963  cubic2  26069  quart1  26077  log2cnv  26165  basellem1  26301  basellem3  26303  basellem5  26305  basellem8  26308  mumul  26401  chtublem  26430  perfectlem1  26448  perfectlem2  26449  perfect  26450  dchrabl  26473  bposlem6  26508  bposlem9  26511  lgsdir2lem4  26547  lgsdir2  26549  lgsquadlem2  26600  lgsquad2  26605  rpvmasum2  26731  mulog2sumlem1  26753  pntibndlem2  26810  pntibndlem3  26811  pntlemf  26824  nvscom  29099  ipasslem11  29310  ipblnfi  29325  hvmulcom  29513  h1de2bi  30024  homul12  30275  riesz3i  30532  riesz1  30535  kbass4  30589  sin2h  35827  heiborlem6  36034  rmym1  40968  expgrowthi  42179  expgrowth  42181  stoweidlem10  43795  perfectALTVlem1  45432  perfectALTVlem2  45433  perfectALTV  45434  tgoldbachlt  45527  2zrngnmlid2  45768