Theorem mulcom 7450

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

Syntax hints:   -> wi 4   /\ wa 102   = wceq 1289   e. wcel 1438  (class class class)co 5634   CCcc 7327   x. cmul 7334

This theorem was proved from axioms:  ax-mulcom 7425

This theorem is referenced by:  adddir  7458  mulid2  7465  mulcomi  7473  mulcomd  7488  mul12  7590  mul32  7591  mul31  7592  muladd  7841  subdir  7843  mul01  7846  mulneg2  7853  recextlem1  8094  divmulap3  8118  div23ap  8132  div13ap  8134  div12ap  8135  divmulasscomap  8137  divcanap4  8140  divmul13ap  8156  divmul24ap  8157  divcanap7  8162  div2negap  8176  prodgt02  8286  prodge02  8288  ltmul2  8289  lemul2  8290  lemul2a  8292  ltmulgt12  8298  lemulge12  8300  ltmuldiv2  8308  ltdivmul2  8311  ledivmul2  8313  lemuldiv2  8315  times2  8515  modqcyc2  9732  subsq  10026  cjmulrcl  10286  imval2  10293  abscj  10450  sqabsadd  10453  sqabssub  10454  dvdsmul1  10900  odd2np1lem  10954  odd2np1  10955  opeo  10979  omeo  10980  modgcd  11064  dvdsgcd  11083  gcdmultiple  11091  coprmdvds  11156  coprmdvds2  11157  qredeq  11160