Theorem mulcom 7164

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

Syntax hints:   -> wi 4   /\ wa 102   = wceq 1285   e. wcel 1434  (class class class)co 5543   CCcc 7041   x. cmul 7048

This theorem was proved from axioms:  ax-mulcom 7139

This theorem is referenced by:  adddir  7172  mulid2  7179  mulcomi  7187  mulcomd  7202  mul12  7304  mul32  7305  mul31  7306  muladd  7555  subdir  7557  mul01  7560  mulneg2  7567  recextlem1  7808  divmulap3  7832  div23ap  7846  div13ap  7848  div12ap  7849  divmulasscomap  7851  divcanap4  7854  divmul13ap  7870  divmul24ap  7871  divcanap7  7876  div2negap  7890  prodgt02  7998  prodge02  8000  ltmul2  8001  lemul2  8002  lemul2a  8004  ltmulgt12  8010  lemulge12  8012  ltmuldiv2  8020  ltdivmul2  8023  ledivmul2  8025  lemuldiv2  8027  times2  8228  modqcyc2  9442  subsq  9678  cjmulrcl  9912  imval2  9919  abscj  10076  sqabsadd  10079  sqabssub  10080  dvdsmul1  10362  odd2np1lem  10416  odd2np1  10417  opeo  10441  omeo  10442  modgcd  10526  dvdsgcd  10545  gcdmultiple  10553  coprmdvds  10618  coprmdvds2  10619  qredeq  10622