Theorem mulcomi 8333

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 8309	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
4	1, 2, 3	mp2an 430	1 |- ( A x. B ) = ( B x. A )

This proof depends on syntax axioms:   = wceq 1402   e. wcel 2209  (class class class)co 6085   CCcc 8178   x. cmul 8185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulcom 8281

This theorem is used by:  mulcomli  8334  8th4div3  9529  numma2c  9832  nummul2c  9836  9t11e99  9916  binom2i  11100  fac3  11186  tanval2ap  12499  pockthi  13160  mod2xnegi  13221  decsplit1  13231  decsplit  13232  83prm  13260  sincosq4sgn  16022  2logb9irrALT  16171  log2ublem2  16183  log2ublem3  16184  log2ublog2  16185  chtqub  16257  bposlem8  16279  2lgsoddprmlem2  16391  2lgsoddprmlem3d  16395