Theorem mulcom 8255

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398   ∈ wcel 2203  (class class class)co 6049  ℂcc 8124   · cmul 8131

This theorem was proved from axioms:  ax-mulcom 8227

This theorem is referenced by:  adddir  8264  mullid  8271  mulcomi  8279  mulcomd  8294  mul12  8401  mul32  8402  mul31  8403  muladd  8656  subdir  8658  mul01  8661  mulneg2  8668  recextlem1  8924  divmulap3  8950  div23ap  8964  div13ap  8966  div12ap  8967  divmulasscomap  8969  divcanap4  8972  divmul13ap  8988  divmul24ap  8989  divcanap7  8994  div2negap  9008  prodgt02  9126  prodge02  9128  ltmul2  9129  lemul2  9130  lemul2a  9132  ltmulgt12  9138  lemulge12  9140  ltmuldiv2  9148  ltdivmul2  9151  ledivmul2  9153  lemuldiv2  9155  times2  9365  modqcyc2  10721  subsq  11007  cjmulrcl  11568  imval2  11575  abscj  11733  sqabsadd  11736  sqabssub  11737  prod3fmul  12223  prodmodclem3  12257  efcllemp  12340  efexp  12364  sinmul  12426  demoivreALT  12456  dvdsmul1  12495  odd2np1lem  12554  odd2np1  12555  opeo  12579  omeo  12580  modgcd  12683  dvdsgcd  12704  gcdmultiple  12712  coprmdvds  12785  coprmdvds2  12786  qredeq  12789  modprm0  12948  modprmn0modprm0  12950  coprimeprodsq2  12952  cncrng  14709  cnfldui  14729  ef2kpi  15663  sinperlem  15665  sinmpi  15672  cosmpi  15673  sinppi  15674  cosppi  15675  cxpcom  15795  perfectlem1  15859  perfectlem2  15860  perfect  15861  lgsdir2lem4  15896  lgsdir2  15898  lgsquadlem2  15943  lgsquad2  15948