Theorem mulcom 8154

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395   ∈ wcel 2200  (class class class)co 6013  ℂcc 8023   · cmul 8030

This theorem was proved from axioms:  ax-mulcom 8126

This theorem is referenced by:  adddir  8163  mullid  8170  mulcomi  8178  mulcomd  8194  mul12  8301  mul32  8302  mul31  8303  muladd  8556  subdir  8558  mul01  8561  mulneg2  8568  recextlem1  8824  divmulap3  8850  div23ap  8864  div13ap  8866  div12ap  8867  divmulasscomap  8869  divcanap4  8872  divmul13ap  8888  divmul24ap  8889  divcanap7  8894  div2negap  8908  prodgt02  9026  prodge02  9028  ltmul2  9029  lemul2  9030  lemul2a  9032  ltmulgt12  9038  lemulge12  9040  ltmuldiv2  9048  ltdivmul2  9051  ledivmul2  9053  lemuldiv2  9055  times2  9265  modqcyc2  10615  subsq  10901  cjmulrcl  11441  imval2  11448  abscj  11606  sqabsadd  11609  sqabssub  11610  prod3fmul  12095  prodmodclem3  12129  efcllemp  12212  efexp  12236  sinmul  12298  demoivreALT  12328  dvdsmul1  12367  odd2np1lem  12426  odd2np1  12427  opeo  12451  omeo  12452  modgcd  12555  dvdsgcd  12576  gcdmultiple  12584  coprmdvds  12657  coprmdvds2  12658  qredeq  12661  modprm0  12820  modprmn0modprm0  12822  coprimeprodsq2  12824  cncrng  14576  cnfldui  14596  ef2kpi  15523  sinperlem  15525  sinmpi  15532  cosmpi  15533  sinppi  15534  cosppi  15535  cxpcom  15655  perfectlem1  15716  perfectlem2  15717  perfect  15718  lgsdir2lem4  15753  lgsdir2  15755  lgsquadlem2  15800  lgsquad2  15805