Theorem mulcomli 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
mulcomli.3	|- ( A x. B ) = C

Assertion

Ref	Expression
mulcomli	|- ( B x. A ) = C

Proof of Theorem mulcomli

Step	Hyp	Ref	Expression
1		axi.2	. . 3 |- B e. CC
2		axi.1	. . 3 |- A e. CC
3	1, 2	mulcomi 8332	. 2 |- ( B x. A ) = ( A x. B )
4		mulcomli.3	. 2 |- ( A x. B ) = C
5	3, 4	eqtri 2259	1 |- ( B x. A ) = C

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-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220  ax-mulcom 8280

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  nummul2c  9826  halfthird  9919  5recm6rec  9920  sq4e2t8  11074  cos2bnd  12527  dec5nprm  13193  karatsuba  13209  2exp6  13212  2exp8  13214  2exp11  13215  2exp16  13216  log2ublem3  16085  log2ublog2  16086  2lgslem3a  16212  2lgsoddprmlem3c  16228  2lgsoddprmlem3d  16229  ex-exp  16741  ex-fac  16742