Theorem mulcom 7621

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

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1299   e. wcel 1448  (class class class)co 5706   CCcc 7498   x. cmul 7505

This theorem was proved from axioms:  ax-mulcom 7596

This theorem is referenced by:  adddir  7629  mulid2  7636  mulcomi  7644  mulcomd  7659  mul12  7762  mul32  7763  mul31  7764  muladd  8013  subdir  8015  mul01  8018  mulneg2  8025  recextlem1  8273  divmulap3  8298  div23ap  8312  div13ap  8314  div12ap  8315  divmulasscomap  8317  divcanap4  8320  divmul13ap  8336  divmul24ap  8337  divcanap7  8342  div2negap  8356  prodgt02  8469  prodge02  8471  ltmul2  8472  lemul2  8473  lemul2a  8475  ltmulgt12  8481  lemulge12  8483  ltmuldiv2  8491  ltdivmul2  8494  ledivmul2  8496  lemuldiv2  8498  times2  8701  modqcyc2  9974  subsq  10240  cjmulrcl  10500  imval2  10507  abscj  10664  sqabsadd  10667  sqabssub  10668  efcllemp  11162  efexp  11186  sinmul  11249  demoivreALT  11277  dvdsmul1  11310  odd2np1lem  11364  odd2np1  11365  opeo  11389  omeo  11390  modgcd  11474  dvdsgcd  11493  gcdmultiple  11501  coprmdvds  11566  coprmdvds2  11567  qredeq  11570