Theorem mulcomli 9624

Description: Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1
axi.2
mulcomli.3

Assertion

Ref	Expression
mulcomli

Proof of Theorem mulcomli

Step	Hyp	Ref	Expression
1		axi.2	. . 3
2		axi.1	. . 3
3	1, 2	mulcomi 9623	. 2
4		mulcomli.3	. 2
5	3, 4	eqtri 2486	1

Syntax hints:  =wceq 1395  e.wcel 1818  (class class class)co 6296  cc 9511  cmul 9518

This theorem is referenced by:  divcan1i  10313  mvllmuli  10402  recgt0ii  10476  nummul2c  11041  cos2bnd  13923  dec5nprm  14552  decexp2  14561  karatsuba  14570  2exp6  14572  2exp8  14574  2exp16  14575  7prm  14596  13prm  14601  17prm  14602  19prm  14603  23prm  14604  43prm  14607  83prm  14608  139prm  14609  163prm  14610  317prm  14611  631prm  14612  1259lem1  14613  1259lem2  14614  1259lem3  14615  1259lem4  14616  1259lem5  14617  1259prm  14618  2503lem1  14619  2503lem2  14620  2503lem3  14621  2503prm  14622  4001lem1  14623  4001lem2  14624  4001lem3  14625  4001lem4  14626  4001prm  14627  pcoass  21524  efif1olem2  22930  mcubic  23178  quart1lem  23186  quart1  23187  quartlem1  23188  tanatan  23250  log2ublem3  23279  log2ub  23280  cht3  23447  bclbnd  23555  bpos1lem  23557  bposlem4  23562  bposlem5  23563  bposlem8  23566  ipasslem10  25754  siii  25768  normlem3  26029  bcsiALT  26096  halfthird  29113  5recm6rec  29114  fouriersw  32014  inductionexd  37967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435  ax-mulcom 9577

This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2449