Theorem mulcom 8151

Description: Alias for ax-mulcom 8123, for naming consistency with mulcomi 8175. (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 8123	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 6013   CCcc 8020   x. cmul 8027

This theorem was proved from axioms:  ax-mulcom 8123

This theorem is referenced by:  adddir  8160  mullid  8167  mulcomi  8175  mulcomd  8191  mul12  8298  mul32  8299  mul31  8300  muladd  8553  subdir  8555  mul01  8558  mulneg2  8565  recextlem1  8821  divmulap3  8847  div23ap  8861  div13ap  8863  div12ap  8864  divmulasscomap  8866  divcanap4  8869  divmul13ap  8885  divmul24ap  8886  divcanap7  8891  div2negap  8905  prodgt02  9023  prodge02  9025  ltmul2  9026  lemul2  9027  lemul2a  9029  ltmulgt12  9035  lemulge12  9037  ltmuldiv2  9045  ltdivmul2  9048  ledivmul2  9050  lemuldiv2  9052  times2  9262  modqcyc2  10612  subsq  10898  cjmulrcl  11438  imval2  11445  abscj  11603  sqabsadd  11606  sqabssub  11607  prod3fmul  12092  prodmodclem3  12126  efcllemp  12209  efexp  12233  sinmul  12295  demoivreALT  12325  dvdsmul1  12364  odd2np1lem  12423  odd2np1  12424  opeo  12448  omeo  12449  modgcd  12552  dvdsgcd  12573  gcdmultiple  12581  coprmdvds  12654  coprmdvds2  12655  qredeq  12658  modprm0  12817  modprmn0modprm0  12819  coprimeprodsq2  12821  cncrng  14573  cnfldui  14593  ef2kpi  15520  sinperlem  15522  sinmpi  15529  cosmpi  15530  sinppi  15531  cosppi  15532  cxpcom  15652  perfectlem1  15713  perfectlem2  15714  perfect  15715  lgsdir2lem4  15750  lgsdir2  15752  lgsquadlem2  15797  lgsquad2  15802