Theorem mulcom 8144

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395   ∈ wcel 2200  (class class class)co 6010  ℂcc 8013   · cmul 8020

This theorem was proved from axioms:  ax-mulcom 8116

This theorem is referenced by:  adddir  8153  mullid  8160  mulcomi  8168  mulcomd  8184  mul12  8291  mul32  8292  mul31  8293  muladd  8546  subdir  8548  mul01  8551  mulneg2  8558  recextlem1  8814  divmulap3  8840  div23ap  8854  div13ap  8856  div12ap  8857  divmulasscomap  8859  divcanap4  8862  divmul13ap  8878  divmul24ap  8879  divcanap7  8884  div2negap  8898  prodgt02  9016  prodge02  9018  ltmul2  9019  lemul2  9020  lemul2a  9022  ltmulgt12  9028  lemulge12  9030  ltmuldiv2  9038  ltdivmul2  9041  ledivmul2  9043  lemuldiv2  9045  times2  9255  modqcyc2  10599  subsq  10885  cjmulrcl  11419  imval2  11426  abscj  11584  sqabsadd  11587  sqabssub  11588  prod3fmul  12073  prodmodclem3  12107  efcllemp  12190  efexp  12214  sinmul  12276  demoivreALT  12306  dvdsmul1  12345  odd2np1lem  12404  odd2np1  12405  opeo  12429  omeo  12430  modgcd  12533  dvdsgcd  12554  gcdmultiple  12562  coprmdvds  12635  coprmdvds2  12636  qredeq  12639  modprm0  12798  modprmn0modprm0  12800  coprimeprodsq2  12802  cncrng  14554  cnfldui  14574  ef2kpi  15501  sinperlem  15503  sinmpi  15510  cosmpi  15511  sinppi  15512  cosppi  15513  cxpcom  15633  perfectlem1  15694  perfectlem2  15695  perfect  15696  lgsdir2lem4  15731  lgsdir2  15733  lgsquadlem2  15778  lgsquad2  15783