Theorem mulcom 8314

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

Assertion

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

Proof of Theorem mulcom

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

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

This proof depends on axioms:  ax-mulcom 8286

This theorem is used by:  adddir  8323  mullid  8330  mulcomi  8338  mulcomd  8353  mul12  8462  mul32  8463  mul31  8464  muladd  8718  subdir  8720  mul01  8723  mulneg2  8730  recextlem1  8987  divmulap3  9015  div23ap  9029  div13ap  9031  div12ap  9032  divmulasscomap  9034  divcanap4  9037  divmul13ap  9053  divmul24ap  9054  divcanap7  9059  div2negap  9073  prodgt02  9191  prodge02  9193  ltmul2  9194  lemul2  9195  lemul2a  9197  ltmulgt12  9203  lemulge12  9205  ltmuldiv2  9213  ltdivmul2  9216  ledivmul2  9218  lemuldiv2  9220  times2  9442  modqcyc2  10818  subsq  11104  cjmulrcl  11674  imval2  11681  abscj  11840  sqabsadd  11843  sqabssub  11844  prod3fmul  12333  prodmodclem3  12367  efcllemp  12450  efexp  12474  sinmul  12536  demoivreALT  12566  dvdsmul1  12605  odd2np1lem  12664  odd2np1  12665  opeo  12689  omeo  12690  modgcd  12793  dvdsgcd  12814  gcdmultiple  12822  coprmdvds  12895  coprmdvds2  12896  qredeq  12899  modprm0  13062  modprmn0modprm0  13064  coprimeprodsq2  13066  cncrng  15015  cnfldui  15033  ef2kpi  16033  sinperlem  16035  sinmpi  16042  cosmpi  16043  sinppi  16044  cosppi  16045  cxpcom  16173  chtublem  16295  perfectlem1  16299  perfectlem2  16300  perfect  16301  bposlem6  16316  bposlem9  16319  lgsdir2lem4  16355  lgsdir2  16357  lgsquadlem2  16402  lgsquad2  16407