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 11683 | . 2 class 4 | |
2 | c3 11682 | . . 3 class 3 | |
3 | c1 10527 | . . 3 class 1 | |
4 | caddc 10529 | . . 3 class + | |
5 | 2, 3, 4 | co 7145 | . 2 class (3 + 1) |
6 | 1, 5 | wceq 1528 | 1 wff 4 = (3 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 4nn 11709 4re 11710 4cn 11711 4pos 11733 4m1e3 11755 2p2e4 11761 3p1e4 11771 3p2e5 11777 4p4e8 11781 5p4e9 11784 3lt4 11800 halfpm6th 11847 6p4e10 12159 7p4e11 12163 7p7e14 12166 8p4e12 12169 8p6e14 12171 9p4e13 12176 9p5e14 12177 4t4e16 12186 5t4e20 12189 6t4e24 12193 7t4e28 12198 8t4e32 12204 9t4e36 12211 fz0to4untppr 13000 4bc2eq6 13679 bpoly3 15402 bpoly4 15403 fsumcube 15404 ef4p 15456 ef01bndlem 15527 ge2nprmge4 16035 lt6abl 18946 cphipval 23775 sincosq4sgn 25016 binom4 25355 quart1lem 25360 log2cnv 25450 ppiublem2 25707 ppiub 25708 chtub 25716 bclbnd 25784 bposlem8 25795 lgsdir2lem3 25831 3wlkdlem1 27866 ipval2 28412 problem3 32808 rmydioph 39491 rmxdioph 39493 expdiophlem2 39499 lt4addmuld 41453 stoweidlem13 42179 4even 43721 sbgoldbo 43799 |
Copyright terms: Public domain | W3C validator |