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 7966 | . 2 class 4 | |
2 | c3 7965 | . . 3 class 3 | |
3 | c1 6890 | . . 3 class 1 | |
4 | caddc 6892 | . . 3 class + | |
5 | 2, 3, 4 | co 5512 | . 2 class (3 + 1) |
6 | 1, 5 | wceq 1243 | 1 wff 4 = (3 + 1) |
Colors of variables: wff set class |
This definition is referenced by: 4re 7992 4pos 8013 2p2e4 8037 3p1e4 8045 3p2e5 8052 4p4e8 8056 5p4e9 8059 6p4e10 8063 4nn 8079 3lt4 8089 halfpm6th 8145 7p4e11 8419 7p7e14 8422 8p4e12 8424 8p6e14 8426 9p4e13 8431 9p5e14 8432 4t4e16 8440 5t4e20 8442 6t4e24 8446 7t4e28 8451 8t4e32 8457 9t4e36 8464 fzo0to42pr 9076 |
Copyright terms: Public domain | W3C validator |