Theorem mulcom 11289

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

Assertion

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

Proof of Theorem mulcom

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11201   · cmul 11208

This proof depends on axioms:  ax-mulcom 11267

This theorem is used by:  adddir  11300  mullid  11310  mulcomi  11320  mulcomd  11333  mul12  11478  mul32  11479  mul31  11480  mul4r  11482  mul01  11492  muladd  11751  subdir  11753  mulneg2  11756  recextlem1  11949  mulcan2g  11973  divmul3  11982  div23  11996  div13  11998  div12  11999  divmulasscom  12001  divcan4  12004  divmul13  12023  divmul24  12024  divcan7  12029  div2neg  12043  prodgt02  12168  ltmul2  12171  lemul2  12173  lemul2a  12175  ltmulgt12  12180  lemulge12  12183  ltmuldiv2  12194  ltdivmul2  12197  lt2mul2div  12198  ledivmul2  12199  lemuldiv2  12201  supmul  12292  times2  12482  modcyc  14049  modcyc2  14050  modmulmodr  14083  subsq  14357  cjmulrcl  15316  imval2  15323  abscj  15451  sqabsadd  15454  sqabssub  15455  sqreulem  15532  iseraltlem2  15855  iseraltlem3  15856  climcndslem2  16024  prodfmul  16064  prodmolem3  16105  bpoly3  16229  efcllem  16248  efexp  16274  sinmul  16345  demoivreALT  16374  dvdsmul1  16452  odd2np1lem  16515  odd2np1  16516  opeo  16540  omeo  16541  modgcd  16710  bezoutlem1  16717  dvdsgcd  16722  coprmdvds  16833  coprmdvds2  16834  qredeq  16837  eulerthlem2  16964  modprm0  16988  modprmn0modprm0  16990  coprimeprodsq2  16992  prmreclem6  17104  odmod  19765  cncrng  21704  cnsrng  21717  pcoass  25350  clmvscom  25416  dvlipcn  26319  plydivlem4  26622  quotcan  26637  aaliou3lem3  26676  ef2kpi  26812  sinperlem  26814  sinmpi  26821  cosmpi  26822  sinppi  26823  cosppi  26824  sineq0  26857  tanregt0  26872  logneg  26921  lognegb  26923  logimul  26947  tanarg  26952  logtayl  26993  cxpsqrtlem  27035  cxpcom  27072  cubic2  27181  quart1  27189  log2cnv  27277  basellem1  27413  basellem3  27415  basellem5  27417  chtublem  27543  perfectlem1  27561  perfectlem2  27562  perfect  27563  dchrabl  27586  bposlem6  27621  bposlem9  27624  lgsdir2lem4  27660  lgsdir2  27662  lgsquadlem2  27713  lgsquad2  27718  rpvmasum2  27844  mulog2sumlem1  27866  pntibndlem2  27923  pntibndlem3  27924  pntlemf  27937  nvscom  31236  ipasslem11  31447  ipblnfi  31462  hvmulcom  31650  h1de2bi  32161  homul12  32412  riesz3i  32669  riesz1  32672  kbass4  32726  sin2h  38626  heiborlem6  38843  rmym1  44035  expgrowthi  45410  expgrowth  45412  stoweidlem10  47113  perfectALTVlem1  48912  perfectALTVlem2  48913  perfectALTV  48914  tgoldbachlt  49007  2zrngnmlid2  49447