Theorem mulcom 8308

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

Assertion

Ref	Expression
mulcom	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )

Proof of Theorem mulcom

Step	Hyp	Ref	Expression
1		ax-mulcom 8280	1 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   = wceq 1402   e. wcel 2209  (class class class)co 6085   CCcc 8177   x. cmul 8184

This proof depends on axioms:  ax-mulcom 8280

This theorem is used by:  adddir  8317  mullid  8324  mulcomi  8332  mulcomd  8347  mul12  8455  mul32  8456  mul31  8457  muladd  8711  subdir  8713  mul01  8716  mulneg2  8723  recextlem1  8979  divmulap3  9007  div23ap  9021  div13ap  9023  div12ap  9024  divmulasscomap  9026  divcanap4  9029  divmul13ap  9045  divmul24ap  9046  divcanap7  9051  div2negap  9065  prodgt02  9183  prodge02  9185  ltmul2  9186  lemul2  9187  lemul2a  9189  ltmulgt12  9195  lemulge12  9197  ltmuldiv2  9205  ltdivmul2  9208  ledivmul2  9210  lemuldiv2  9212  times2  9433  modqcyc2  10797  subsq  11083  cjmulrcl  11652  imval2  11659  abscj  11818  sqabsadd  11821  sqabssub  11822  prod3fmul  12308  prodmodclem3  12342  efcllemp  12425  efexp  12449  sinmul  12511  demoivreALT  12541  dvdsmul1  12580  odd2np1lem  12639  odd2np1  12640  opeo  12664  omeo  12665  modgcd  12768  dvdsgcd  12789  gcdmultiple  12797  coprmdvds  12870  coprmdvds2  12871  qredeq  12874  modprm0  13033  modprmn0modprm0  13035  coprimeprodsq2  13037  cncrng  14906  cnfldui  14924  ef2kpi  15908  sinperlem  15910  sinmpi  15917  cosmpi  15918  sinppi  15919  cosppi  15920  cxpcom  16044  perfectlem1  16117  perfectlem2  16118  perfect  16119  lgsdir2lem4  16154  lgsdir2  16156  lgsquadlem2  16201  lgsquad2  16206