Theorem mulcomi 10046

Description: Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1	|- A e. CC
axi.2	|- B e. CC

Assertion

Ref	Expression
mulcomi	|- ( A x. B ) = ( B x. A )

Proof of Theorem mulcomi

Step	Hyp	Ref	Expression
1		axi.1	. 2 |- A e. CC
2		axi.2	. 2 |- B e. CC
3		mulcom 10022	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
4	1, 2, 3	mp2an 708	1 |- ( A x. B ) = ( B x. A )

Syntax hints:   = wceq 1483   e. wcel 1990  (class class class)co 6650   CCcc 9934   x. cmul 9941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 10000

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  mulcomli  10047  divmul13i  10786  8th4div3  11252  numma2c  11559  nummul2c  11563  9t11e99  11671  9t11e99OLD  11672  binom2i  12974  fac3  13067  tanval2  14863  pockthi  15611  mod2xnegi  15775  decexp2  15779  decsplit1  15786  decsplit  15787  decsplit1OLD  15790  decsplitOLD  15791  83prm  15830  dvsincos  23744  sincosq4sgn  24253  ang180lem3  24541  mcubic  24574  cubic2  24575  log2ublem2  24674  log2ublem3  24675  log2ub  24676  basellem8  24814  ppiub  24929  chtub  24937  bposlem8  25016  2lgsoddprmlem2  25134  2lgsoddprmlem3d  25138  ax5seglem7  25815  ex-exp  27307  ex-ind-dvds  27318  ipdirilem  27684  siilem1  27706  bcseqi  27977  h1de2i  28412  dpmul10  29603  dpmul4  29622  signswch  30638  hgt750lem  30729  hgt750lem2  30730  problem4  31562  problem5  31563  quad3  31564  arearect  37801  areaquad  37802  wallispilem4  40285  dirkercncflem1  40320  fourierswlem  40447  257prm  41473  fmtno4prmfac  41484  5tcu2e40  41532  41prothprm  41536  tgoldbachlt  41704  tgoldbachltOLD  41710  zlmodzxzequap  42288