Theorem mulcom 8308

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

Assertion

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

Proof of Theorem mulcom

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   = wceq 1402   ∈ wcel 2209  (class class class)co 6085  ℂcc 8177   · cmul 8184

This proof depends on axioms:  ax-mulcom 8280

This theorem is used by:  adddir  8317  mullid  8324  mulcomi  8332  mulcomd  8347  mul12  8456  mul32  8457  mul31  8458  muladd  8712  subdir  8714  mul01  8717  mulneg2  8724  recextlem1  8981  divmulap3  9009  div23ap  9023  div13ap  9025  div12ap  9026  divmulasscomap  9028  divcanap4  9031  divmul13ap  9047  divmul24ap  9048  divcanap7  9053  div2negap  9067  prodgt02  9185  prodge02  9187  ltmul2  9188  lemul2  9189  lemul2a  9191  ltmulgt12  9197  lemulge12  9199  ltmuldiv2  9207  ltdivmul2  9210  ledivmul2  9212  lemuldiv2  9214  times2  9435  modqcyc2  10810  subsq  11096  cjmulrcl  11666  imval2  11673  abscj  11832  sqabsadd  11835  sqabssub  11836  prod3fmul  12324  prodmodclem3  12358  efcllemp  12441  efexp  12465  sinmul  12527  demoivreALT  12557  dvdsmul1  12596  odd2np1lem  12655  odd2np1  12656  opeo  12680  omeo  12681  modgcd  12784  dvdsgcd  12805  gcdmultiple  12813  coprmdvds  12886  coprmdvds2  12887  qredeq  12890  modprm0  13053  modprmn0modprm0  13055  coprimeprodsq2  13057  cncrng  14955  cnfldui  14973  ef2kpi  15957  sinperlem  15959  sinmpi  15966  cosmpi  15967  sinppi  15968  cosppi  15969  cxpcom  16093  perfectlem1  16197  perfectlem2  16198  perfect  16199  lgsdir2lem4  16248  lgsdir2  16250  lgsquadlem2  16295  lgsquad2  16300