Theorem mulcom 11161

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073   · cmul 11080

This theorem was proved from axioms:  ax-mulcom 11139

This theorem is referenced by:  adddir  11172  mullid  11180  mulcomi  11189  mulcomd  11202  mul12  11346  mul32  11347  mul31  11348  mul4r  11350  mul01  11360  muladd  11617  subdir  11619  mulneg2  11622  recextlem1  11815  mulcan2g  11839  divmul3  11849  div23  11863  div13  11865  div12  11866  divmulasscom  11868  divcan4  11871  divmul13  11892  divmul24  11893  divcan7  11898  div2neg  11912  prodgt02  12037  ltmul2  12040  lemul2  12042  lemul2a  12044  ltmulgt12  12050  lemulge12  12053  ltmuldiv2  12064  ltdivmul2  12067  lt2mul2div  12068  ledivmul2  12069  lemuldiv2  12071  supmul  12162  times2  12325  modcyc  13875  modcyc2  13876  modmulmodr  13909  subsq  14182  cjmulrcl  15117  imval2  15124  abscj  15252  sqabsadd  15255  sqabssub  15256  sqreulem  15333  iseraltlem2  15656  iseraltlem3  15657  climcndslem2  15823  prodfmul  15863  prodmolem3  15906  bpoly3  16031  efcllem  16050  efexp  16076  sinmul  16147  demoivreALT  16176  dvdsmul1  16254  odd2np1lem  16317  odd2np1  16318  opeo  16342  omeo  16343  modgcd  16509  bezoutlem1  16516  dvdsgcd  16521  coprmdvds  16630  coprmdvds2  16631  qredeq  16634  eulerthlem2  16759  modprm0  16783  modprmn0modprm0  16785  coprimeprodsq2  16787  prmreclem6  16899  odmod  19483  cncrng  21307  cncrngOLD  21308  cnsrng  21324  pcoass  24931  clmvscom  24997  dvlipcn  25906  plydivlem4  26211  quotcan  26224  aaliou3lem3  26259  ef2kpi  26394  sinperlem  26396  sinmpi  26403  cosmpi  26404  sinppi  26405  cosppi  26406  sineq0  26440  tanregt0  26455  logneg  26504  lognegb  26506  logimul  26530  tanarg  26535  logtayl  26576  cxpsqrtlem  26618  cxpcom  26655  cubic2  26765  quart1  26773  log2cnv  26861  basellem1  26998  basellem3  27000  basellem5  27002  basellem8  27005  mumul  27098  chtublem  27129  perfectlem1  27147  perfectlem2  27148  perfect  27149  dchrabl  27172  bposlem6  27207  bposlem9  27210  lgsdir2lem4  27246  lgsdir2  27248  lgsquadlem2  27299  lgsquad2  27304  rpvmasum2  27430  mulog2sumlem1  27452  pntibndlem2  27509  pntibndlem3  27510  pntlemf  27523  nvscom  30565  ipasslem11  30776  ipblnfi  30791  hvmulcom  30979  h1de2bi  31490  homul12  31741  riesz3i  31998  riesz1  32001  kbass4  32055  sin2h  37611  heiborlem6  37817  rmym1  42931  expgrowthi  44329  expgrowth  44331  stoweidlem10  46015  perfectALTVlem1  47726  perfectALTVlem2  47727  perfectALTV  47728  tgoldbachlt  47821  2zrngnmlid2  48249