Theorem mulcom 8124

Description: Alias for ax-mulcom 8096, for naming consistency with mulcomi 8148. (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 8096	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 6000   CCcc 7993   x. cmul 8000

This theorem was proved from axioms:  ax-mulcom 8096

This theorem is referenced by:  adddir  8133  mullid  8140  mulcomi  8148  mulcomd  8164  mul12  8271  mul32  8272  mul31  8273  muladd  8526  subdir  8528  mul01  8531  mulneg2  8538  recextlem1  8794  divmulap3  8820  div23ap  8834  div13ap  8836  div12ap  8837  divmulasscomap  8839  divcanap4  8842  divmul13ap  8858  divmul24ap  8859  divcanap7  8864  div2negap  8878  prodgt02  8996  prodge02  8998  ltmul2  8999  lemul2  9000  lemul2a  9002  ltmulgt12  9008  lemulge12  9010  ltmuldiv2  9018  ltdivmul2  9021  ledivmul2  9023  lemuldiv2  9025  times2  9235  modqcyc2  10577  subsq  10863  cjmulrcl  11393  imval2  11400  abscj  11558  sqabsadd  11561  sqabssub  11562  prod3fmul  12047  prodmodclem3  12081  efcllemp  12164  efexp  12188  sinmul  12250  demoivreALT  12280  dvdsmul1  12319  odd2np1lem  12378  odd2np1  12379  opeo  12403  omeo  12404  modgcd  12507  dvdsgcd  12528  gcdmultiple  12536  coprmdvds  12609  coprmdvds2  12610  qredeq  12613  modprm0  12772  modprmn0modprm0  12774  coprimeprodsq2  12776  cncrng  14527  cnfldui  14547  ef2kpi  15474  sinperlem  15476  sinmpi  15483  cosmpi  15484  sinppi  15485  cosppi  15486  cxpcom  15606  perfectlem1  15667  perfectlem2  15668  perfect  15669  lgsdir2lem4  15704  lgsdir2  15706  lgsquadlem2  15751  lgsquad2  15756