Theorem mulcom 11204

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

Assertion

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

Proof of Theorem mulcom

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  (class class class)co 7423  ℂcc 11116   · cmul 11123

This proof depends on axioms:  ax-mulcom 11182

This theorem is used by:  adddir  11215  mullid  11225  mulcomi  11235  mulcomd  11248  mul12  11393  mul32  11394  mul31  11395  mul4r  11397  mul01  11407  muladd  11664  subdir  11666  mulneg2  11669  recextlem1  11862  mulcan2g  11886  divmul3  11895  div23  11909  div13  11911  div12  11912  divmulasscom  11914  divcan4  11917  divmul13  11936  divmul24  11937  divcan7  11942  div2neg  11956  prodgt02  12081  ltmul2  12084  lemul2  12086  lemul2a  12088  ltmulgt12  12093  lemulge12  12096  ltmuldiv2  12107  ltdivmul2  12110  lt2mul2div  12111  ledivmul2  12112  lemuldiv2  12114  supmul  12205  times2  12395  modcyc  13959  modcyc2  13960  modmulmodr  13993  subsq  14266  cjmulrcl  15221  imval2  15228  abscj  15356  sqabsadd  15359  sqabssub  15360  sqreulem  15437  iseraltlem2  15760  iseraltlem3  15761  climcndslem2  15930  prodfmul  15970  prodmolem3  16013  bpoly3  16137  efcllem  16156  efexp  16182  sinmul  16253  demoivreALT  16282  dvdsmul1  16360  odd2np1lem  16423  odd2np1  16424  opeo  16448  omeo  16449  modgcd  16615  bezoutlem1  16622  dvdsgcd  16627  coprmdvds  16736  coprmdvds2  16737  qredeq  16740  eulerthlem2  16866  modprm0  16890  modprmn0modprm0  16892  coprimeprodsq2  16894  prmreclem6  17006  odmod  19647  cncrng  21580  cnsrng  21593  pcoass  25220  clmvscom  25286  dvlipcn  26190  plydivlem4  26494  quotcan  26507  aaliou3lem3  26544  ef2kpi  26680  sinperlem  26682  sinmpi  26689  cosmpi  26690  sinppi  26691  cosppi  26692  sineq0  26726  tanregt0  26741  logneg  26790  lognegb  26792  logimul  26816  tanarg  26821  logtayl  26862  cxpsqrtlem  26904  cxpcom  26941  cubic2  27050  quart1  27058  log2cnv  27146  basellem1  27282  basellem3  27284  basellem5  27286  mumul  27382  chtublem  27412  perfectlem1  27430  perfectlem2  27431  perfect  27432  dchrabl  27455  bposlem6  27490  bposlem9  27493  lgsdir2lem4  27529  lgsdir2  27531  lgsquadlem2  27582  lgsquad2  27587  rpvmasum2  27713  mulog2sumlem1  27735  pntibndlem2  27792  pntibndlem3  27793  pntlemf  27806  nvscom  31018  ipasslem11  31229  ipblnfi  31244  hvmulcom  31432  h1de2bi  31943  homul12  32194  riesz3i  32451  riesz1  32454  kbass4  32508  sin2h  38301  heiborlem6  38507  rmym1  43702  expgrowthi  45083  expgrowth  45085  stoweidlem10  46764  perfectALTVlem1  48526  perfectALTVlem2  48527  perfectALTV  48528  tgoldbachlt  48621  2zrngnmlid2  49062