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  14990  cnfldui  15008  ef2kpi  15999  sinperlem  16001  sinmpi  16008  cosmpi  16009  sinppi  16010  cosppi  16011  cxpcom  16135  chtublem  16256  perfectlem1  16260  perfectlem2  16261  perfect  16262  bposlem6  16277  bposlem9  16280  lgsdir2lem4  16316  lgsdir2  16318  lgsquadlem2  16363  lgsquad2  16368