Theorem mulcom 8161

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1397   e. wcel 2202  (class class class)co 6018   CCcc 8030   x. cmul 8037

This theorem was proved from axioms:  ax-mulcom 8133

This theorem is referenced by:  adddir  8170  mullid  8177  mulcomi  8185  mulcomd  8201  mul12  8308  mul32  8309  mul31  8310  muladd  8563  subdir  8565  mul01  8568  mulneg2  8575  recextlem1  8831  divmulap3  8857  div23ap  8871  div13ap  8873  div12ap  8874  divmulasscomap  8876  divcanap4  8879  divmul13ap  8895  divmul24ap  8896  divcanap7  8901  div2negap  8915  prodgt02  9033  prodge02  9035  ltmul2  9036  lemul2  9037  lemul2a  9039  ltmulgt12  9045  lemulge12  9047  ltmuldiv2  9055  ltdivmul2  9058  ledivmul2  9060  lemuldiv2  9062  times2  9272  modqcyc2  10623  subsq  10909  cjmulrcl  11465  imval2  11472  abscj  11630  sqabsadd  11633  sqabssub  11634  prod3fmul  12120  prodmodclem3  12154  efcllemp  12237  efexp  12261  sinmul  12323  demoivreALT  12353  dvdsmul1  12392  odd2np1lem  12451  odd2np1  12452  opeo  12476  omeo  12477  modgcd  12580  dvdsgcd  12601  gcdmultiple  12609  coprmdvds  12682  coprmdvds2  12683  qredeq  12686  modprm0  12845  modprmn0modprm0  12847  coprimeprodsq2  12849  cncrng  14602  cnfldui  14622  ef2kpi  15549  sinperlem  15551  sinmpi  15558  cosmpi  15559  sinppi  15560  cosppi  15561  cxpcom  15681  perfectlem1  15742  perfectlem2  15743  perfect  15744  lgsdir2lem4  15779  lgsdir2  15781  lgsquadlem2  15826  lgsquad2  15831