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  9528  numma2c  9831  nummul2c  9835  9t11e99  9915  binom2i  11098  fac3  11184  tanval2ap  12496  pockthi  13157  mod2xnegi  13218  decsplit1  13228  decsplit  13229  83prm  13257  sincosq4sgn  15980  2logb9irrALT  16129  log2ublem2  16141  log2ublem3  16142  log2ublog2  16143  2lgsoddprmlem2  16323  2lgsoddprmlem3d  16327