Theorem mulcom 8139

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1395   e. wcel 2200  (class class class)co 6007   CCcc 8008   x. cmul 8015

This theorem was proved from axioms:  ax-mulcom 8111

This theorem is referenced by:  adddir  8148  mullid  8155  mulcomi  8163  mulcomd  8179  mul12  8286  mul32  8287  mul31  8288  muladd  8541  subdir  8543  mul01  8546  mulneg2  8553  recextlem1  8809  divmulap3  8835  div23ap  8849  div13ap  8851  div12ap  8852  divmulasscomap  8854  divcanap4  8857  divmul13ap  8873  divmul24ap  8874  divcanap7  8879  div2negap  8893  prodgt02  9011  prodge02  9013  ltmul2  9014  lemul2  9015  lemul2a  9017  ltmulgt12  9023  lemulge12  9025  ltmuldiv2  9033  ltdivmul2  9036  ledivmul2  9038  lemuldiv2  9040  times2  9250  modqcyc2  10594  subsq  10880  cjmulrcl  11413  imval2  11420  abscj  11578  sqabsadd  11581  sqabssub  11582  prod3fmul  12067  prodmodclem3  12101  efcllemp  12184  efexp  12208  sinmul  12270  demoivreALT  12300  dvdsmul1  12339  odd2np1lem  12398  odd2np1  12399  opeo  12423  omeo  12424  modgcd  12527  dvdsgcd  12548  gcdmultiple  12556  coprmdvds  12629  coprmdvds2  12630  qredeq  12633  modprm0  12792  modprmn0modprm0  12794  coprimeprodsq2  12796  cncrng  14548  cnfldui  14568  ef2kpi  15495  sinperlem  15497  sinmpi  15504  cosmpi  15505  sinppi  15506  cosppi  15507  cxpcom  15627  perfectlem1  15688  perfectlem2  15689  perfect  15690  lgsdir2lem4  15725  lgsdir2  15727  lgsquadlem2  15772  lgsquad2  15777