Theorem mulcomi 8338

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 8314	. 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 6088   CCcc 8183   x. cmul 8190

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

This theorem is used by:  mulcomli  8339  8th4div3  9535  numma2c  9837  nummul2c  9841  9t11e99  9921  binom2i  11105  fac3  11191  tanval2ap  12504  pockthi  13165  mod2xnegi  13226  decsplit1  13236  decsplit  13237  83prm  13265  sincosq4sgn  16073  2logb9irrALT  16227  log2ublem2  16239  log2ublem3  16240  log2ublog2  16241  chtqub  16313  bposlem8  16335  2lgsoddprmlem2  16447  2lgsoddprmlem3d  16451