![]() |
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 12321 | . 2 class 4 | |
2 | c3 12320 | . . 3 class 3 | |
3 | c1 11159 | . . 3 class 1 | |
4 | caddc 11161 | . . 3 class + | |
5 | 2, 3, 4 | co 7424 | . 2 class (3 + 1) |
6 | 1, 5 | wceq 1534 | 1 wff 4 = (3 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 4nn 12347 4re 12348 4cn 12349 4pos 12371 4m1e3 12393 2p2e4 12399 3p1e4 12409 3p2e5 12415 4p4e8 12419 5p4e9 12422 3lt4 12438 halfpm6th 12485 6p4e10 12801 7p4e11 12805 7p7e14 12808 8p4e12 12811 8p6e14 12813 9p4e13 12818 9p5e14 12819 4t4e16 12828 5t4e20 12831 6t4e24 12835 7t4e28 12840 8t4e32 12846 9t4e36 12853 fz0to4untppr 13658 4bc2eq6 14346 bpoly3 16060 bpoly4 16061 fsumcube 16062 ef4p 16115 ef01bndlem 16186 ge2nprmge4 16702 lt6abl 19893 cphipval 25262 sincosq4sgn 26529 binom4 26878 quart1lem 26883 log2cnv 26972 ppiublem2 27232 ppiub 27233 chtub 27241 bclbnd 27309 bposlem8 27320 lgsdir2lem3 27356 3wlkdlem1 30092 ipval2 30640 problem3 35495 aks4d1p1p7 41773 rmydioph 42672 rmxdioph 42674 expdiophlem2 42680 lt4addmuld 44921 stoweidlem13 45634 4even 47281 sbgoldbo 47359 ackval40 48081 ackval41a 48082 ackval42 48084 |
Copyright terms: Public domain | W3C validator |