![]() |
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 11490 | . 2 class 4 | |
2 | c3 11489 | . . 3 class 3 | |
3 | c1 10328 | . . 3 class 1 | |
4 | caddc 10330 | . . 3 class + | |
5 | 2, 3, 4 | co 6970 | . 2 class (3 + 1) |
6 | 1, 5 | wceq 1507 | 1 wff 4 = (3 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 4nn 11517 4re 11518 4cn 11519 4pos 11547 4m1e3 11569 2p2e4 11575 3p1e4 11585 3p2e5 11591 4p4e8 11595 5p4e9 11598 3lt4 11614 halfpm6th 11661 6p4e10 11978 7p4e11 11982 7p7e14 11985 8p4e12 11988 8p6e14 11990 9p4e13 11995 9p5e14 11996 4t4e16 12005 5t4e20 12008 6t4e24 12012 7t4e28 12017 8t4e32 12023 9t4e36 12030 fz0to4untppr 12819 4bc2eq6 13497 bpoly3 15262 bpoly4 15263 fsumcube 15264 ef4p 15316 ef01bndlem 15387 ge2nprmge4 15891 lt6abl 18759 cphipval 23539 sincosq4sgn 24780 binom4 25119 quart1lem 25124 log2cnv 25214 ppiublem2 25471 ppiub 25472 chtub 25480 bclbnd 25548 bposlem8 25559 lgsdir2lem3 25595 3wlkdlem1 27678 ipval2 28251 problem3 32370 rmydioph 38952 rmxdioph 38954 expdiophlem2 38960 lt4addmuld 40948 stoweidlem13 41675 4even 43182 sbgoldbo 43260 |
Copyright terms: Public domain | W3C validator |