Theorem mulcom 8204

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398   ∈ wcel 2202  (class class class)co 6028  ℂcc 8073   · cmul 8080

This theorem was proved from axioms:  ax-mulcom 8176

This theorem is referenced by:  adddir  8213  mullid  8220  mulcomi  8228  mulcomd  8244  mul12  8351  mul32  8352  mul31  8353  muladd  8606  subdir  8608  mul01  8611  mulneg2  8618  recextlem1  8874  divmulap3  8900  div23ap  8914  div13ap  8916  div12ap  8917  divmulasscomap  8919  divcanap4  8922  divmul13ap  8938  divmul24ap  8939  divcanap7  8944  div2negap  8958  prodgt02  9076  prodge02  9078  ltmul2  9079  lemul2  9080  lemul2a  9082  ltmulgt12  9088  lemulge12  9090  ltmuldiv2  9098  ltdivmul2  9101  ledivmul2  9103  lemuldiv2  9105  times2  9315  modqcyc2  10666  subsq  10952  cjmulrcl  11508  imval2  11515  abscj  11673  sqabsadd  11676  sqabssub  11677  prod3fmul  12163  prodmodclem3  12197  efcllemp  12280  efexp  12304  sinmul  12366  demoivreALT  12396  dvdsmul1  12435  odd2np1lem  12494  odd2np1  12495  opeo  12519  omeo  12520  modgcd  12623  dvdsgcd  12644  gcdmultiple  12652  coprmdvds  12725  coprmdvds2  12726  qredeq  12729  modprm0  12888  modprmn0modprm0  12890  coprimeprodsq2  12892  cncrng  14645  cnfldui  14665  ef2kpi  15597  sinperlem  15599  sinmpi  15606  cosmpi  15607  sinppi  15608  cosppi  15609  cxpcom  15729  perfectlem1  15793  perfectlem2  15794  perfect  15795  lgsdir2lem4  15830  lgsdir2  15832  lgsquadlem2  15877  lgsquad2  15882