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  15907  sinperlem  15909  sinmpi  15916  cosmpi  15917  sinppi  15918  cosppi  15919  cxpcom  16040  perfectlem1  16113  perfectlem2  16114  perfect  16115  lgsdir2lem4  16150  lgsdir2  16152  lgsquadlem2  16197  lgsquad2  16202