Theorem mulcom 7971

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1364   e. wcel 2160  (class class class)co 5897   CCcc 7840   x. cmul 7847

This theorem was proved from axioms:  ax-mulcom 7943

This theorem is referenced by:  adddir  7979  mullid  7986  mulcomi  7994  mulcomd  8010  mul12  8117  mul32  8118  mul31  8119  muladd  8372  subdir  8374  mul01  8377  mulneg2  8384  recextlem1  8639  divmulap3  8665  div23ap  8679  div13ap  8681  div12ap  8682  divmulasscomap  8684  divcanap4  8687  divmul13ap  8703  divmul24ap  8704  divcanap7  8709  div2negap  8723  prodgt02  8841  prodge02  8843  ltmul2  8844  lemul2  8845  lemul2a  8847  ltmulgt12  8853  lemulge12  8855  ltmuldiv2  8863  ltdivmul2  8866  ledivmul2  8868  lemuldiv2  8870  times2  9079  modqcyc2  10393  subsq  10661  cjmulrcl  10931  imval2  10938  abscj  11096  sqabsadd  11099  sqabssub  11100  prod3fmul  11584  prodmodclem3  11618  efcllemp  11701  efexp  11725  sinmul  11787  demoivreALT  11816  dvdsmul1  11855  odd2np1lem  11912  odd2np1  11913  opeo  11937  omeo  11938  modgcd  12027  dvdsgcd  12048  gcdmultiple  12056  coprmdvds  12127  coprmdvds2  12128  qredeq  12131  modprm0  12289  modprmn0modprm0  12291  coprimeprodsq2  12293  cncrng  13889  ef2kpi  14704  sinperlem  14706  sinmpi  14713  cosmpi  14714  sinppi  14715  cosppi  14716  cxpcom  14834  lgsdir2lem4  14910  lgsdir2  14912