Theorem mulcom 7102

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

Syntax hints:   -> wi 4   /\ wa 102   = wceq 1284   e. wcel 1433  (class class class)co 5532   CCcc 6979   x. cmul 6986

This theorem was proved from axioms:  ax-mulcom 7077

This theorem is referenced by:  adddir  7110  mulid2  7117  mulcomi  7125  mulcomd  7140  mul12  7237  mul32  7238  mul31  7239  muladd  7488  subdir  7490  mul01  7493  mulneg2  7500  recextlem1  7741  divmulap3  7765  div23ap  7779  div13ap  7781  div12ap  7782  divmulasscomap  7784  divcanap4  7787  divmul13ap  7803  divmul24ap  7804  divcanap7  7809  div2negap  7823  prodgt02  7931  prodge02  7933  ltmul2  7934  lemul2  7935  lemul2a  7937  ltmulgt12  7943  lemulge12  7945  ltmuldiv2  7953  ltdivmul2  7956  ledivmul2  7958  lemuldiv2  7960  times2  8161  modqcyc2  9362  subsq  9581  cjmulrcl  9774  imval2  9781  abscj  9938  sqabsadd  9941  sqabssub  9942  dvdsmul1  10217  odd2np1lem  10271  odd2np1  10272  opeo  10297  omeo  10298  modgcd  10382  dvdsgcd  10401  gcdmultiple  10409  coprmdvds  10474  coprmdvds2  10475  qredeq  10478