Theorem mulcomli 8339

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

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 8286

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

This theorem is used by:  2t3e6  9471  2t4e8  9474  nummul2c  9841  halfthird  9934  5recm6rec  9935  sq4e2t8  11094  cos2bnd  12551  dec5nprm  13221  karatsuba  13238  2exp6  13241  2exp8  13243  2exp11  13244  2exp16  13245  13prm  13258  17prm  13259  19prm  13260  23prm  13261  43prm  13264  83prm  13265  139prm  13266  163prm  13267  317prm  13268  631prm  13269  1259lem1  13270  1259lem2  13271  1259lem3  13272  1259lem4  13273  1259lem5  13274  1259prm  13275  log2ublem3  16240  log2ublog2  16241  bclbnd  16324  bpos1lem  16326  bposlem4  16331  bposlem5  16332  bposlem8  16335  2lgslem3a  16434  2lgsoddprmlem3c  16450  2lgsoddprmlem3d  16451  ex-exp  16963  ex-fac  16964