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 8773 | . 2 class 4 | |
2 | c3 8772 | . . 3 class 3 | |
3 | c1 7621 | . . 3 class 1 | |
4 | caddc 7623 | . . 3 class + | |
5 | 2, 3, 4 | co 5774 | . 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 8797 4pos 8817 4m1e3 8841 2p2e4 8847 3p1e4 8855 3p2e5 8861 4p4e8 8865 5p4e9 8868 4nn 8883 3lt4 8892 halfpm6th 8940 6p4e10 9253 7p4e11 9257 7p7e14 9260 8p4e12 9263 8p6e14 9265 9p4e13 9270 9p5e14 9271 4t4e16 9280 5t4e20 9283 6t4e24 9287 7t4e28 9292 8t4e32 9298 9t4e36 9305 fzo0to42pr 9997 4bc2eq6 10520 ef4p 11400 ef01bndlem 11463 sincosq4sgn 12910 |
Copyright terms: Public domain | W3C validator |