Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-4 | Structured version Visualization version GIF version |
Description: Define the number 4. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-4 | ⊢ 4 = (3 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c4 10949 | . 2 class 4 | |
2 | c3 10948 | . . 3 class 3 | |
3 | c1 9816 | . . 3 class 1 | |
4 | caddc 9818 | . . 3 class + | |
5 | 2, 3, 4 | co 6549 | . 2 class (3 + 1) |
6 | 1, 5 | wceq 1475 | 1 wff 4 = (3 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 4re 10974 4pos 10993 4m1e3 11015 2p2e4 11021 3p1e4 11030 3p2e5 11037 4p4e8 11041 5p4e9 11044 6p4e10OLD 11048 4nn 11064 3lt4 11074 halfpm6th 11130 6p4e10 11474 7p4e11 11481 7p4e11OLD 11482 7p7e14 11485 8p4e12 11490 8p6e14 11492 9p4e13 11498 9p5e14 11499 4t4e16 11509 5t4e20 11513 5t4e20OLD 11514 6t4e24 11519 7t4e28 11526 8t4e32 11532 9t4e36 11541 fz0to4untppr 12311 fzo0to42pr 12422 4bc2eq6 12978 bpoly3 14628 bpoly4 14629 fsumcube 14630 ef4p 14682 ef01bndlem 14753 lt6abl 18119 cphipval 22850 iblitg 23341 sincosq4sgn 24057 ang180lem2 24340 binom4 24377 quart1lem 24382 log2cnv 24471 ppiublem2 24728 ppiub 24729 chtub 24737 bclbnd 24805 bposlem8 24816 lgsdir2lem3 24852 ipval2 26946 problem3 30815 rmydioph 36599 rmxdioph 36601 expdiophlem2 36607 lt4addmuld 38461 stoweidlem13 38906 4even 40156 31wlkdlem1 41326 |
Copyright terms: Public domain | W3C validator |