Theorem mulcom 8256

Description: Alias for ax-mulcom 8228, for naming consistency with mulcomi 8280. (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 8228	1 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1398   e. wcel 2203  (class class class)co 6050   CCcc 8125   x. cmul 8132

This theorem was proved from axioms:  ax-mulcom 8228

This theorem is referenced by:  adddir  8265  mullid  8272  mulcomi  8280  mulcomd  8295  mul12  8402  mul32  8403  mul31  8404  muladd  8657  subdir  8659  mul01  8662  mulneg2  8669  recextlem1  8925  divmulap3  8951  div23ap  8965  div13ap  8967  div12ap  8968  divmulasscomap  8970  divcanap4  8973  divmul13ap  8989  divmul24ap  8990  divcanap7  8995  div2negap  9009  prodgt02  9127  prodge02  9129  ltmul2  9130  lemul2  9131  lemul2a  9133  ltmulgt12  9139  lemulge12  9141  ltmuldiv2  9149  ltdivmul2  9152  ledivmul2  9154  lemuldiv2  9156  times2  9366  modqcyc2  10722  subsq  11008  cjmulrcl  11572  imval2  11579  abscj  11737  sqabsadd  11740  sqabssub  11741  prod3fmul  12227  prodmodclem3  12261  efcllemp  12344  efexp  12368  sinmul  12430  demoivreALT  12460  dvdsmul1  12499  odd2np1lem  12558  odd2np1  12559  opeo  12583  omeo  12584  modgcd  12687  dvdsgcd  12708  gcdmultiple  12716  coprmdvds  12789  coprmdvds2  12790  qredeq  12793  modprm0  12952  modprmn0modprm0  12954  coprimeprodsq2  12956  cncrng  14717  cnfldui  14737  ef2kpi  15671  sinperlem  15673  sinmpi  15680  cosmpi  15681  sinppi  15682  cosppi  15683  cxpcom  15803  perfectlem1  15867  perfectlem2  15868  perfect  15869  lgsdir2lem4  15904  lgsdir2  15906  lgsquadlem2  15951  lgsquad2  15956