Theorem mulcom 7890

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

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1348   e. wcel 2141  (class class class)co 5850   CCcc 7759   x. cmul 7766

This theorem was proved from axioms:  ax-mulcom 7862

This theorem is referenced by:  adddir  7898  mulid2  7905  mulcomi  7913  mulcomd  7928  mul12  8035  mul32  8036  mul31  8037  muladd  8290  subdir  8292  mul01  8295  mulneg2  8302  recextlem1  8556  divmulap3  8581  div23ap  8595  div13ap  8597  div12ap  8598  divmulasscomap  8600  divcanap4  8603  divmul13ap  8619  divmul24ap  8620  divcanap7  8625  div2negap  8639  prodgt02  8756  prodge02  8758  ltmul2  8759  lemul2  8760  lemul2a  8762  ltmulgt12  8768  lemulge12  8770  ltmuldiv2  8778  ltdivmul2  8781  ledivmul2  8783  lemuldiv2  8785  times2  8994  modqcyc2  10303  subsq  10569  cjmulrcl  10838  imval2  10845  abscj  11003  sqabsadd  11006  sqabssub  11007  prod3fmul  11491  prodmodclem3  11525  efcllemp  11608  efexp  11632  sinmul  11694  demoivreALT  11723  dvdsmul1  11762  odd2np1lem  11818  odd2np1  11819  opeo  11843  omeo  11844  modgcd  11933  dvdsgcd  11954  gcdmultiple  11962  coprmdvds  12033  coprmdvds2  12034  qredeq  12037  modprm0  12195  modprmn0modprm0  12197  coprimeprodsq2  12199  ef2kpi  13442  sinperlem  13444  sinmpi  13451  cosmpi  13452  sinppi  13453  cosppi  13454  cxpcom  13572  lgsdir2lem4  13647  lgsdir2  13649