Theorem mulcom 8160

Description: Alias for ax-mulcom 8132, for naming consistency with mulcomi 8184. (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 8132	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 6017   CCcc 8029   x. cmul 8036

This theorem was proved from axioms:  ax-mulcom 8132

This theorem is referenced by:  adddir  8169  mullid  8176  mulcomi  8184  mulcomd  8200  mul12  8307  mul32  8308  mul31  8309  muladd  8562  subdir  8564  mul01  8567  mulneg2  8574  recextlem1  8830  divmulap3  8856  div23ap  8870  div13ap  8872  div12ap  8873  divmulasscomap  8875  divcanap4  8878  divmul13ap  8894  divmul24ap  8895  divcanap7  8900  div2negap  8914  prodgt02  9032  prodge02  9034  ltmul2  9035  lemul2  9036  lemul2a  9038  ltmulgt12  9044  lemulge12  9046  ltmuldiv2  9054  ltdivmul2  9057  ledivmul2  9059  lemuldiv2  9061  times2  9271  modqcyc2  10621  subsq  10907  cjmulrcl  11447  imval2  11454  abscj  11612  sqabsadd  11615  sqabssub  11616  prod3fmul  12101  prodmodclem3  12135  efcllemp  12218  efexp  12242  sinmul  12304  demoivreALT  12334  dvdsmul1  12373  odd2np1lem  12432  odd2np1  12433  opeo  12457  omeo  12458  modgcd  12561  dvdsgcd  12582  gcdmultiple  12590  coprmdvds  12663  coprmdvds2  12664  qredeq  12667  modprm0  12826  modprmn0modprm0  12828  coprimeprodsq2  12830  cncrng  14582  cnfldui  14602  ef2kpi  15529  sinperlem  15531  sinmpi  15538  cosmpi  15539  sinppi  15540  cosppi  15541  cxpcom  15661  perfectlem1  15722  perfectlem2  15723  perfect  15724  lgsdir2lem4  15759  lgsdir2  15761  lgsquadlem2  15806  lgsquad2  15811