Theorem mulcom 8161

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1397   ∈ wcel 2202  (class class class)co 6018  ℂcc 8030   · cmul 8037

This theorem was proved from axioms:  ax-mulcom 8133

This theorem is referenced by:  adddir  8170  mullid  8177  mulcomi  8185  mulcomd  8201  mul12  8308  mul32  8309  mul31  8310  muladd  8563  subdir  8565  mul01  8568  mulneg2  8575  recextlem1  8831  divmulap3  8857  div23ap  8871  div13ap  8873  div12ap  8874  divmulasscomap  8876  divcanap4  8879  divmul13ap  8895  divmul24ap  8896  divcanap7  8901  div2negap  8915  prodgt02  9033  prodge02  9035  ltmul2  9036  lemul2  9037  lemul2a  9039  ltmulgt12  9045  lemulge12  9047  ltmuldiv2  9055  ltdivmul2  9058  ledivmul2  9060  lemuldiv2  9062  times2  9272  modqcyc2  10623  subsq  10909  cjmulrcl  11449  imval2  11456  abscj  11614  sqabsadd  11617  sqabssub  11618  prod3fmul  12104  prodmodclem3  12138  efcllemp  12221  efexp  12245  sinmul  12307  demoivreALT  12337  dvdsmul1  12376  odd2np1lem  12435  odd2np1  12436  opeo  12460  omeo  12461  modgcd  12564  dvdsgcd  12585  gcdmultiple  12593  coprmdvds  12666  coprmdvds2  12667  qredeq  12670  modprm0  12829  modprmn0modprm0  12831  coprimeprodsq2  12833  cncrng  14586  cnfldui  14606  ef2kpi  15533  sinperlem  15535  sinmpi  15542  cosmpi  15543  sinppi  15544  cosppi  15545  cxpcom  15665  perfectlem1  15726  perfectlem2  15727  perfect  15728  lgsdir2lem4  15763  lgsdir2  15765  lgsquadlem2  15810  lgsquad2  15815