Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mulcomli | Structured version Visualization version Unicode version |
Description: Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Ref | Expression |
---|---|
axi.1 | |
axi.2 | |
mulcomli.3 |
Ref | Expression |
---|---|
mulcomli |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axi.2 | . . 3 | |
2 | axi.1 | . . 3 | |
3 | 1, 2 | mulcomi 10046 | . 2 |
4 | mulcomli.3 | . 2 | |
5 | 3, 4 | eqtri 2644 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wceq 1483 wcel 1990 (class class class)co 6650 cc 9934 cmul 9941 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-ext 2602 ax-mulcom 10000 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-cleq 2615 |
This theorem is referenced by: divcan1i 10769 mvllmuli 10858 recgt0ii 10929 nummul2c 11563 halfthird 11685 5recm6rec 11686 sq4e2t8 12962 cos2bnd 14918 prmo3 15745 dec5nprm 15770 decexp2 15779 karatsuba 15792 karatsubaOLD 15793 2exp6 15795 2exp8 15796 2exp16 15797 7prm 15817 13prm 15823 17prm 15824 19prm 15825 23prm 15826 43prm 15829 83prm 15830 139prm 15831 163prm 15832 317prm 15833 631prm 15834 1259lem1 15838 1259lem2 15839 1259lem3 15840 1259lem4 15841 1259lem5 15842 1259prm 15843 2503lem1 15844 2503lem2 15845 2503lem3 15846 2503prm 15847 4001lem1 15848 4001lem2 15849 4001lem3 15850 4001lem4 15851 4001prm 15852 pcoass 22824 efif1olem2 24289 mcubic 24574 quart1lem 24582 quart1 24583 quartlem1 24584 tanatan 24646 log2ublem3 24675 log2ub 24676 cht3 24899 bclbnd 25005 bpos1lem 25007 bposlem4 25012 bposlem5 25013 bposlem8 25016 2lgslem3a 25121 2lgsoddprmlem3c 25137 2lgsoddprmlem3d 25138 ex-fac 27308 ex-prmo 27316 ipasslem10 27694 siii 27708 normlem3 27969 bcsiALT 28036 dpmul1000 29607 hgt750lem2 30730 inductionexd 38453 fouriersw 40448 1t10e1p1e11 41319 1t10e1p1e11OLD 41320 fmtno5lem1 41465 fmtno5lem2 41466 257prm 41473 fmtno4prmfac 41484 fmtno4nprmfac193 41486 fmtno5faclem2 41492 139prmALT 41511 127prm 41515 2exp11 41517 mod42tp1mod8 41519 3exp4mod41 41533 41prothprmlem2 41535 |
Copyright terms: Public domain | W3C validator |