Theorem mulcomli 8334

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 8333	. 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 8178   x. cmul 8185

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 8281

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

This theorem is used by:  2t3e6  9465  2t4e8  9468  nummul2c  9836  halfthird  9929  5recm6rec  9930  sq4e2t8  11089  cos2bnd  12546  dec5nprm  13216  karatsuba  13233  2exp6  13236  2exp8  13238  2exp11  13239  2exp16  13240  13prm  13253  17prm  13254  19prm  13255  23prm  13256  43prm  13259  83prm  13260  139prm  13261  163prm  13262  317prm  13263  631prm  13264  1259lem1  13265  1259lem2  13266  1259lem3  13267  1259lem4  13268  1259lem5  13269  1259prm  13270  log2ublem3  16184  log2ublog2  16185  bclbnd  16268  bpos1lem  16270  bposlem4  16275  bposlem5  16276  bposlem8  16279  2lgslem3a  16378  2lgsoddprmlem3c  16394  2lgsoddprmlem3d  16395  ex-exp  16907  ex-fac  16908