Theorem mulcom 8136

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395   ∈ wcel 2200  (class class class)co 6007  ℂcc 8005   · cmul 8012

This theorem was proved from axioms:  ax-mulcom 8108

This theorem is referenced by:  adddir  8145  mullid  8152  mulcomi  8160  mulcomd  8176  mul12  8283  mul32  8284  mul31  8285  muladd  8538  subdir  8540  mul01  8543  mulneg2  8550  recextlem1  8806  divmulap3  8832  div23ap  8846  div13ap  8848  div12ap  8849  divmulasscomap  8851  divcanap4  8854  divmul13ap  8870  divmul24ap  8871  divcanap7  8876  div2negap  8890  prodgt02  9008  prodge02  9010  ltmul2  9011  lemul2  9012  lemul2a  9014  ltmulgt12  9020  lemulge12  9022  ltmuldiv2  9030  ltdivmul2  9033  ledivmul2  9035  lemuldiv2  9037  times2  9247  modqcyc2  10590  subsq  10876  cjmulrcl  11406  imval2  11413  abscj  11571  sqabsadd  11574  sqabssub  11575  prod3fmul  12060  prodmodclem3  12094  efcllemp  12177  efexp  12201  sinmul  12263  demoivreALT  12293  dvdsmul1  12332  odd2np1lem  12391  odd2np1  12392  opeo  12416  omeo  12417  modgcd  12520  dvdsgcd  12541  gcdmultiple  12549  coprmdvds  12622  coprmdvds2  12623  qredeq  12626  modprm0  12785  modprmn0modprm0  12787  coprimeprodsq2  12789  cncrng  14541  cnfldui  14561  ef2kpi  15488  sinperlem  15490  sinmpi  15497  cosmpi  15498  sinppi  15499  cosppi  15500  cxpcom  15620  perfectlem1  15681  perfectlem2  15682  perfect  15683  lgsdir2lem4  15718  lgsdir2  15720  lgsquadlem2  15765  lgsquad2  15770