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  9842  halfthird  9935  5recm6rec  9936  sq4e2t8  11095  cos2bnd  12552  dec5nprm  13222  karatsuba  13239  2exp6  13242  2exp8  13244  2exp11  13245  2exp16  13246  13prm  13259  17prm  13260  19prm  13261  23prm  13262  43prm  13265  83prm  13266  139prm  13267  163prm  13268  317prm  13269  631prm  13270  1259lem1  13271  1259lem2  13272  1259lem3  13273  1259lem4  13274  1259lem5  13275  1259prm  13276  log2ublem3  16223  log2ublog2  16224  bclbnd  16307  bpos1lem  16309  bposlem4  16314  bposlem5  16315  bposlem8  16318  2lgslem3a  16417  2lgsoddprmlem3c  16433  2lgsoddprmlem3d  16434  ex-exp  16946  ex-fac  16947