Theorem mulcom 8309

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

Assertion

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

Proof of Theorem mulcom

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

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

This proof depends on axioms:  ax-mulcom 8281

This theorem is used by:  adddir  8318  mullid  8325  mulcomi  8333  mulcomd  8348  mul12  8457  mul32  8458  mul31  8459  muladd  8713  subdir  8715  mul01  8718  mulneg2  8725  recextlem1  8982  divmulap3  9010  div23ap  9024  div13ap  9026  div12ap  9027  divmulasscomap  9029  divcanap4  9032  divmul13ap  9048  divmul24ap  9049  divcanap7  9054  div2negap  9068  prodgt02  9186  prodge02  9188  ltmul2  9189  lemul2  9190  lemul2a  9192  ltmulgt12  9198  lemulge12  9200  ltmuldiv2  9208  ltdivmul2  9211  ledivmul2  9213  lemuldiv2  9215  times2  9436  modqcyc2  10812  subsq  11098  cjmulrcl  11668  imval2  11675  abscj  11834  sqabsadd  11837  sqabssub  11838  prod3fmul  12327  prodmodclem3  12361  efcllemp  12444  efexp  12468  sinmul  12530  demoivreALT  12560  dvdsmul1  12599  odd2np1lem  12658  odd2np1  12659  opeo  12683  omeo  12684  modgcd  12787  dvdsgcd  12808  gcdmultiple  12816  coprmdvds  12889  coprmdvds2  12890  qredeq  12893  modprm0  13056  modprmn0modprm0  13058  coprimeprodsq2  13060  cncrng  14997  cnfldui  15015  ef2kpi  16007  sinperlem  16009  sinmpi  16016  cosmpi  16017  sinppi  16018  cosppi  16019  cxpcom  16147  chtublem  16269  perfectlem1  16273  perfectlem2  16274  perfect  16275  bposlem6  16290  bposlem9  16293  lgsdir2lem4  16329  lgsdir2  16331  lgsquadlem2  16376  lgsquad2  16381