Theorem mulcom 8128

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1395   e. wcel 2200  (class class class)co 6001   CCcc 7997   x. cmul 8004

This theorem was proved from axioms:  ax-mulcom 8100

This theorem is referenced by:  adddir  8137  mullid  8144  mulcomi  8152  mulcomd  8168  mul12  8275  mul32  8276  mul31  8277  muladd  8530  subdir  8532  mul01  8535  mulneg2  8542  recextlem1  8798  divmulap3  8824  div23ap  8838  div13ap  8840  div12ap  8841  divmulasscomap  8843  divcanap4  8846  divmul13ap  8862  divmul24ap  8863  divcanap7  8868  div2negap  8882  prodgt02  9000  prodge02  9002  ltmul2  9003  lemul2  9004  lemul2a  9006  ltmulgt12  9012  lemulge12  9014  ltmuldiv2  9022  ltdivmul2  9025  ledivmul2  9027  lemuldiv2  9029  times2  9239  modqcyc2  10582  subsq  10868  cjmulrcl  11398  imval2  11405  abscj  11563  sqabsadd  11566  sqabssub  11567  prod3fmul  12052  prodmodclem3  12086  efcllemp  12169  efexp  12193  sinmul  12255  demoivreALT  12285  dvdsmul1  12324  odd2np1lem  12383  odd2np1  12384  opeo  12408  omeo  12409  modgcd  12512  dvdsgcd  12533  gcdmultiple  12541  coprmdvds  12614  coprmdvds2  12615  qredeq  12618  modprm0  12777  modprmn0modprm0  12779  coprimeprodsq2  12781  cncrng  14533  cnfldui  14553  ef2kpi  15480  sinperlem  15482  sinmpi  15489  cosmpi  15490  sinppi  15491  cosppi  15492  cxpcom  15612  perfectlem1  15673  perfectlem2  15674  perfect  15675  lgsdir2lem4  15710  lgsdir2  15712  lgsquadlem2  15757  lgsquad2  15762