Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-4 | Unicode version |
Description: Define the number 4. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-4 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c4 8737 | . 2 | |
2 | c3 8736 | . . 3 | |
3 | c1 7589 | . . 3 | |
4 | caddc 7591 | . . 3 | |
5 | 2, 3, 4 | co 5742 | . 2 |
6 | 1, 5 | wceq 1316 | 1 |
Colors of variables: wff set class |
This definition is referenced by: 4re 8761 4pos 8781 2p2e4 8805 3p1e4 8813 3p2e5 8819 4p4e8 8823 5p4e9 8826 4nn 8841 3lt4 8850 halfpm6th 8898 6p4e10 9211 7p4e11 9215 7p7e14 9218 8p4e12 9221 8p6e14 9223 9p4e13 9228 9p5e14 9229 4t4e16 9238 5t4e20 9241 6t4e24 9245 7t4e28 9250 8t4e32 9256 9t4e36 9263 fzo0to42pr 9952 4bc2eq6 10475 ef4p 11314 ef01bndlem 11377 sincosq4sgn 12821 |
Copyright terms: Public domain | W3C validator |