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 12030 | . 2 class 4 | |
2 | c3 12029 | . . 3 class 3 | |
3 | c1 10873 | . . 3 class 1 | |
4 | caddc 10875 | . . 3 class + | |
5 | 2, 3, 4 | co 7271 | . 2 class (3 + 1) |
6 | 1, 5 | wceq 1542 | 1 wff 4 = (3 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 4nn 12056 4re 12057 4cn 12058 4pos 12080 4m1e3 12102 2p2e4 12108 3p1e4 12118 3p2e5 12124 4p4e8 12128 5p4e9 12131 3lt4 12147 halfpm6th 12194 6p4e10 12508 7p4e11 12512 7p7e14 12515 8p4e12 12518 8p6e14 12520 9p4e13 12525 9p5e14 12526 4t4e16 12535 5t4e20 12538 6t4e24 12542 7t4e28 12547 8t4e32 12553 9t4e36 12560 fz0to4untppr 13358 4bc2eq6 14041 bpoly3 15766 bpoly4 15767 fsumcube 15768 ef4p 15820 ef01bndlem 15891 ge2nprmge4 16404 lt6abl 19494 cphipval 24405 sincosq4sgn 25656 binom4 25998 quart1lem 26003 log2cnv 26092 ppiublem2 26349 ppiub 26350 chtub 26358 bclbnd 26426 bposlem8 26437 lgsdir2lem3 26473 3wlkdlem1 28519 ipval2 29065 problem3 33621 aks4d1p1p7 40079 rmydioph 40833 rmxdioph 40835 expdiophlem2 40841 lt4addmuld 42816 stoweidlem13 43525 4even 45130 sbgoldbo 45208 ackval40 46008 ackval41a 46009 ackval42 46011 |
Copyright terms: Public domain | W3C validator |