Theorem mulcom 8089

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1373   e. wcel 2178  (class class class)co 5967   CCcc 7958   x. cmul 7965

This theorem was proved from axioms:  ax-mulcom 8061

This theorem is referenced by:  adddir  8098  mullid  8105  mulcomi  8113  mulcomd  8129  mul12  8236  mul32  8237  mul31  8238  muladd  8491  subdir  8493  mul01  8496  mulneg2  8503  recextlem1  8759  divmulap3  8785  div23ap  8799  div13ap  8801  div12ap  8802  divmulasscomap  8804  divcanap4  8807  divmul13ap  8823  divmul24ap  8824  divcanap7  8829  div2negap  8843  prodgt02  8961  prodge02  8963  ltmul2  8964  lemul2  8965  lemul2a  8967  ltmulgt12  8973  lemulge12  8975  ltmuldiv2  8983  ltdivmul2  8986  ledivmul2  8988  lemuldiv2  8990  times2  9200  modqcyc2  10542  subsq  10828  cjmulrcl  11313  imval2  11320  abscj  11478  sqabsadd  11481  sqabssub  11482  prod3fmul  11967  prodmodclem3  12001  efcllemp  12084  efexp  12108  sinmul  12170  demoivreALT  12200  dvdsmul1  12239  odd2np1lem  12298  odd2np1  12299  opeo  12323  omeo  12324  modgcd  12427  dvdsgcd  12448  gcdmultiple  12456  coprmdvds  12529  coprmdvds2  12530  qredeq  12533  modprm0  12692  modprmn0modprm0  12694  coprimeprodsq2  12696  cncrng  14446  cnfldui  14466  ef2kpi  15393  sinperlem  15395  sinmpi  15402  cosmpi  15403  sinppi  15404  cosppi  15405  cxpcom  15525  perfectlem1  15586  perfectlem2  15587  perfect  15588  lgsdir2lem4  15623  lgsdir2  15625  lgsquadlem2  15670  lgsquad2  15675