Theorem mulcom 7878

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1343   ∈ wcel 2136  (class class class)co 5841  ℂcc 7747   · cmul 7754

This theorem was proved from axioms:  ax-mulcom 7850

This theorem is referenced by:  adddir  7886  mulid2  7893  mulcomi  7901  mulcomd  7916  mul12  8023  mul32  8024  mul31  8025  muladd  8278  subdir  8280  mul01  8283  mulneg2  8290  recextlem1  8544  divmulap3  8569  div23ap  8583  div13ap  8585  div12ap  8586  divmulasscomap  8588  divcanap4  8591  divmul13ap  8607  divmul24ap  8608  divcanap7  8613  div2negap  8627  prodgt02  8744  prodge02  8746  ltmul2  8747  lemul2  8748  lemul2a  8750  ltmulgt12  8756  lemulge12  8758  ltmuldiv2  8766  ltdivmul2  8769  ledivmul2  8771  lemuldiv2  8773  times2  8982  modqcyc2  10291  subsq  10557  cjmulrcl  10825  imval2  10832  abscj  10990  sqabsadd  10993  sqabssub  10994  prod3fmul  11478  prodmodclem3  11512  efcllemp  11595  efexp  11619  sinmul  11681  demoivreALT  11710  dvdsmul1  11749  odd2np1lem  11805  odd2np1  11806  opeo  11830  omeo  11831  modgcd  11920  dvdsgcd  11941  gcdmultiple  11949  coprmdvds  12020  coprmdvds2  12021  qredeq  12024  modprm0  12182  modprmn0modprm0  12184  coprimeprodsq2  12186  ef2kpi  13327  sinperlem  13329  sinmpi  13336  cosmpi  13337  sinppi  13338  cosppi  13339  cxpcom  13457  lgsdir2lem4  13532  lgsdir2  13534