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  10817  subsq  11103  cjmulrcl  11673  imval2  11680  abscj  11839  sqabsadd  11842  sqabssub  11843  prod3fmul  12332  prodmodclem3  12366  efcllemp  12449  efexp  12473  sinmul  12535  demoivreALT  12565  dvdsmul1  12604  odd2np1lem  12663  odd2np1  12664  opeo  12688  omeo  12689  modgcd  12792  dvdsgcd  12813  gcdmultiple  12821  coprmdvds  12894  coprmdvds2  12895  qredeq  12898  modprm0  13061  modprmn0modprm0  13063  coprimeprodsq2  13065  cncrng  15014  cnfldui  15032  ef2kpi  16050  sinperlem  16052  sinmpi  16059  cosmpi  16060  sinppi  16061  cosppi  16062  cxpcom  16190  chtublem  16312  perfectlem1  16316  perfectlem2  16317  perfect  16318  bposlem6  16333  bposlem9  16336  lgsdir2lem4  16372  lgsdir2  16374  lgsquadlem2  16419  lgsquad2  16424