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  9838  nummul2c  9842  9t11e99  9922  binom2i  11106  fac3  11192  tanval2ap  12505  pockthi  13166  mod2xnegi  13227  decsplit1  13237  decsplit  13238  83prm  13266  sincosq4sgn  16056  2logb9irrALT  16210  log2ublem2  16222  log2ublem3  16223  log2ublog2  16224  chtqub  16296  bposlem8  16318  2lgsoddprmlem2  16430  2lgsoddprmlem3d  16434