Theorem mulcom 11146

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  (class class class)co 7362  ℂcc 11058   · cmul 11065

This theorem was proved from axioms:  ax-mulcom 11124

This theorem is referenced by:  adddir  11155  mullid  11163  mulcomi  11172  mulcomd  11185  mul12  11329  mul32  11330  mul31  11331  mul4r  11333  mul01  11343  muladd  11596  subdir  11598  mulneg2  11601  recextlem1  11794  mulcan2g  11818  divmul3  11827  div23  11841  div13  11843  div12  11844  divmulasscom  11846  divcan4  11849  divmul13  11867  divmul24  11868  divcan7  11873  div2neg  11887  prodgt02  12012  ltmul2  12015  lemul2  12017  lemul2a  12019  ltmulgt12  12025  lemulge12  12027  ltmuldiv2  12038  ltdivmul2  12041  lt2mul2div  12042  ledivmul2  12043  lemuldiv2  12045  supmul  12136  times2  12299  modcyc  13821  modcyc2  13822  modmulmodr  13852  subsq  14124  cjmulrcl  15041  imval2  15048  abscj  15176  sqabsadd  15179  sqabssub  15180  sqreulem  15256  iseraltlem2  15579  iseraltlem3  15580  climcndslem2  15746  prodfmul  15786  prodmolem3  15827  bpoly3  15952  efcllem  15971  efexp  15994  sinmul  16065  demoivreALT  16094  dvdsmul1  16171  odd2np1lem  16233  odd2np1  16234  opeo  16258  omeo  16259  modgcd  16424  bezoutlem1  16431  dvdsgcd  16436  coprmdvds  16540  coprmdvds2  16541  qredeq  16544  eulerthlem2  16665  modprm0  16688  modprmn0modprm0  16690  coprimeprodsq2  16692  prmreclem6  16804  odmod  19342  cncrng  20855  cnsrng  20868  pcoass  24424  clmvscom  24490  dvlipcn  25395  plydivlem4  25693  quotcan  25706  aaliou3lem3  25741  ef2kpi  25872  sinperlem  25874  sinmpi  25881  cosmpi  25882  sinppi  25883  cosppi  25884  sineq0  25917  tanregt0  25932  logneg  25980  lognegb  25982  logimul  26006  tanarg  26011  logtayl  26052  cxpsqrtlem  26094  cxpcom  26129  cubic2  26235  quart1  26243  log2cnv  26331  basellem1  26467  basellem3  26469  basellem5  26471  basellem8  26474  mumul  26567  chtublem  26596  perfectlem1  26614  perfectlem2  26615  perfect  26616  dchrabl  26639  bposlem6  26674  bposlem9  26677  lgsdir2lem4  26713  lgsdir2  26715  lgsquadlem2  26766  lgsquad2  26771  rpvmasum2  26897  mulog2sumlem1  26919  pntibndlem2  26976  pntibndlem3  26977  pntlemf  26990  nvscom  29634  ipasslem11  29845  ipblnfi  29860  hvmulcom  30048  h1de2bi  30559  homul12  30810  riesz3i  31067  riesz1  31070  kbass4  31124  sin2h  36141  heiborlem6  36348  rmym1  41317  expgrowthi  42735  expgrowth  42737  stoweidlem10  44371  perfectALTVlem1  46033  perfectALTVlem2  46034  perfectALTV  46035  tgoldbachlt  46128  2zrngnmlid2  46369