Theorem mulcom 7742

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

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1331   e. wcel 1480  (class class class)co 5767   CCcc 7611   x. cmul 7618

This theorem was proved from axioms:  ax-mulcom 7714

This theorem is referenced by:  adddir  7750  mulid2  7757  mulcomi  7765  mulcomd  7780  mul12  7884  mul32  7885  mul31  7886  muladd  8139  subdir  8141  mul01  8144  mulneg2  8151  recextlem1  8405  divmulap3  8430  div23ap  8444  div13ap  8446  div12ap  8447  divmulasscomap  8449  divcanap4  8452  divmul13ap  8468  divmul24ap  8469  divcanap7  8474  div2negap  8488  prodgt02  8604  prodge02  8606  ltmul2  8607  lemul2  8608  lemul2a  8610  ltmulgt12  8616  lemulge12  8618  ltmuldiv2  8626  ltdivmul2  8629  ledivmul2  8631  lemuldiv2  8633  times2  8842  modqcyc2  10126  subsq  10392  cjmulrcl  10652  imval2  10659  abscj  10817  sqabsadd  10820  sqabssub  10821  prod3fmul  11303  efcllemp  11353  efexp  11377  sinmul  11440  demoivreALT  11469  dvdsmul1  11504  odd2np1lem  11558  odd2np1  11559  opeo  11583  omeo  11584  modgcd  11668  dvdsgcd  11689  gcdmultiple  11697  coprmdvds  11762  coprmdvds2  11763  qredeq  11766  ef2kpi  12876  sinperlem  12878  sinmpi  12885  cosmpi  12886  sinppi  12887  cosppi  12888