Theorem mulcom 8067

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1373   ∈ wcel 2177  (class class class)co 5954  ℂcc 7936   · cmul 7943

This theorem was proved from axioms:  ax-mulcom 8039

This theorem is referenced by:  adddir  8076  mullid  8083  mulcomi  8091  mulcomd  8107  mul12  8214  mul32  8215  mul31  8216  muladd  8469  subdir  8471  mul01  8474  mulneg2  8481  recextlem1  8737  divmulap3  8763  div23ap  8777  div13ap  8779  div12ap  8780  divmulasscomap  8782  divcanap4  8785  divmul13ap  8801  divmul24ap  8802  divcanap7  8807  div2negap  8821  prodgt02  8939  prodge02  8941  ltmul2  8942  lemul2  8943  lemul2a  8945  ltmulgt12  8951  lemulge12  8953  ltmuldiv2  8961  ltdivmul2  8964  ledivmul2  8966  lemuldiv2  8968  times2  9178  modqcyc2  10518  subsq  10804  cjmulrcl  11248  imval2  11255  abscj  11413  sqabsadd  11416  sqabssub  11417  prod3fmul  11902  prodmodclem3  11936  efcllemp  12019  efexp  12043  sinmul  12105  demoivreALT  12135  dvdsmul1  12174  odd2np1lem  12233  odd2np1  12234  opeo  12258  omeo  12259  modgcd  12362  dvdsgcd  12383  gcdmultiple  12391  coprmdvds  12464  coprmdvds2  12465  qredeq  12468  modprm0  12627  modprmn0modprm0  12629  coprimeprodsq2  12631  cncrng  14381  cnfldui  14401  ef2kpi  15328  sinperlem  15330  sinmpi  15337  cosmpi  15338  sinppi  15339  cosppi  15340  cxpcom  15460  perfectlem1  15521  perfectlem2  15522  perfect  15523  lgsdir2lem4  15558  lgsdir2  15560  lgsquadlem2  15605  lgsquad2  15610