Theorem mulcom 8054

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1373   e. wcel 2176  (class class class)co 5944   CCcc 7923   x. cmul 7930

This theorem was proved from axioms:  ax-mulcom 8026

This theorem is referenced by:  adddir  8063  mullid  8070  mulcomi  8078  mulcomd  8094  mul12  8201  mul32  8202  mul31  8203  muladd  8456  subdir  8458  mul01  8461  mulneg2  8468  recextlem1  8724  divmulap3  8750  div23ap  8764  div13ap  8766  div12ap  8767  divmulasscomap  8769  divcanap4  8772  divmul13ap  8788  divmul24ap  8789  divcanap7  8794  div2negap  8808  prodgt02  8926  prodge02  8928  ltmul2  8929  lemul2  8930  lemul2a  8932  ltmulgt12  8938  lemulge12  8940  ltmuldiv2  8948  ltdivmul2  8951  ledivmul2  8953  lemuldiv2  8955  times2  9165  modqcyc2  10505  subsq  10791  cjmulrcl  11198  imval2  11205  abscj  11363  sqabsadd  11366  sqabssub  11367  prod3fmul  11852  prodmodclem3  11886  efcllemp  11969  efexp  11993  sinmul  12055  demoivreALT  12085  dvdsmul1  12124  odd2np1lem  12183  odd2np1  12184  opeo  12208  omeo  12209  modgcd  12312  dvdsgcd  12333  gcdmultiple  12341  coprmdvds  12414  coprmdvds2  12415  qredeq  12418  modprm0  12577  modprmn0modprm0  12579  coprimeprodsq2  12581  cncrng  14331  cnfldui  14351  ef2kpi  15278  sinperlem  15280  sinmpi  15287  cosmpi  15288  sinppi  15289  cosppi  15290  cxpcom  15410  perfectlem1  15471  perfectlem2  15472  perfect  15473  lgsdir2lem4  15508  lgsdir2  15510  lgsquadlem2  15555  lgsquad2  15560