Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-4 | 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 8766 | . 2 class 4 | |
2 | c3 8765 | . . 3 class 3 | |
3 | c1 7614 | . . 3 class 1 | |
4 | caddc 7616 | . . 3 class + | |
5 | 2, 3, 4 | co 5767 | . 2 class (3 + 1) |
6 | 1, 5 | wceq 1331 | 1 wff 4 = (3 + 1) |
Colors of variables: wff set class |
This definition is referenced by: 4re 8790 4pos 8810 4m1e3 8834 2p2e4 8840 3p1e4 8848 3p2e5 8854 4p4e8 8858 5p4e9 8861 4nn 8876 3lt4 8885 halfpm6th 8933 6p4e10 9246 7p4e11 9250 7p7e14 9253 8p4e12 9256 8p6e14 9258 9p4e13 9263 9p5e14 9264 4t4e16 9273 5t4e20 9276 6t4e24 9280 7t4e28 9285 8t4e32 9291 9t4e36 9298 fzo0to42pr 9990 4bc2eq6 10513 ef4p 11389 ef01bndlem 11452 sincosq4sgn 12899 |
Copyright terms: Public domain | W3C validator |