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:  2t3e6  9464  2t4e8  9467  nummul2c  9835  halfthird  9928  5recm6rec  9929  sq4e2t8  11087  cos2bnd  12543  dec5nprm  13213  karatsuba  13230  2exp6  13233  2exp8  13235  2exp11  13236  2exp16  13237  13prm  13250  17prm  13251  19prm  13252  23prm  13253  43prm  13256  83prm  13257  139prm  13258  163prm  13259  317prm  13260  631prm  13261  1259lem1  13262  1259lem2  13263  1259lem3  13264  1259lem4  13265  1259lem5  13266  1259prm  13267  log2ublem3  16142  log2ublog2  16143  bclbnd  16205  bpos1lem  16207  bposlem4  16212  bposlem5  16213  2lgslem3a  16310  2lgsoddprmlem3c  16326  2lgsoddprmlem3d  16327  ex-exp  16839  ex-fac  16840