Theorem mulcom 8272

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398   ∈ wcel 2205  (class class class)co 6058  ℂcc 8141   · cmul 8148

This theorem was proved from axioms:  ax-mulcom 8244

This theorem is referenced by:  adddir  8281  mullid  8288  mulcomi  8296  mulcomd  8311  mul12  8418  mul32  8419  mul31  8420  muladd  8674  subdir  8676  mul01  8679  mulneg2  8686  recextlem1  8942  divmulap3  8968  div23ap  8982  div13ap  8984  div12ap  8985  divmulasscomap  8987  divcanap4  8990  divmul13ap  9006  divmul24ap  9007  divcanap7  9012  div2negap  9026  prodgt02  9144  prodge02  9146  ltmul2  9147  lemul2  9148  lemul2a  9150  ltmulgt12  9156  lemulge12  9158  ltmuldiv2  9166  ltdivmul2  9169  ledivmul2  9171  lemuldiv2  9173  times2  9383  modqcyc2  10746  subsq  11032  cjmulrcl  11597  imval2  11604  abscj  11762  sqabsadd  11765  sqabssub  11766  prod3fmul  12252  prodmodclem3  12286  efcllemp  12369  efexp  12393  sinmul  12455  demoivreALT  12485  dvdsmul1  12524  odd2np1lem  12583  odd2np1  12584  opeo  12608  omeo  12609  modgcd  12712  dvdsgcd  12733  gcdmultiple  12741  coprmdvds  12814  coprmdvds2  12815  qredeq  12818  modprm0  12977  modprmn0modprm0  12979  coprimeprodsq2  12981  cncrng  14829  cnfldui  14849  ef2kpi  15783  sinperlem  15785  sinmpi  15792  cosmpi  15793  sinppi  15794  cosppi  15795  cxpcom  15915  perfectlem1  15979  perfectlem2  15980  perfect  15981  lgsdir2lem4  16016  lgsdir2  16018  lgsquadlem2  16063  lgsquad2  16068