Theorem mulcomi 8332

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 8308	. 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 8177   x. cmul 8184

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

This theorem is used by:  mulcomli  8333  8th4div3  9524  numma2c  9822  nummul2c  9826  9t11e99  9906  binom2i  11085  fac3  11170  tanval2ap  12480  pockthi  13137  decsplit1  13207  decsplit  13208  sincosq4sgn  15930  2logb9irrALT  16076  log2ublem2  16084  log2ublem3  16085  log2ublog2  16086  2lgsoddprmlem2  16225  2lgsoddprmlem3d  16229