![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-7 | GIF version |
Description: Define the number 7. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-7 | ⊢ 7 = (6 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c7 8973 | . 2 class 7 | |
2 | c6 8972 | . . 3 class 6 | |
3 | c1 7811 | . . 3 class 1 | |
4 | caddc 7813 | . . 3 class + | |
5 | 2, 3, 4 | co 5874 | . 2 class (6 + 1) |
6 | 1, 5 | wceq 1353 | 1 wff 7 = (6 + 1) |
Colors of variables: wff set class |
This definition is referenced by: 7re 9000 7pos 9019 7m1e6 9041 6p1e7 9055 4p3e7 9061 5p2e7 9063 6p2e8 9066 7nn 9083 6lt7 9101 7p7e14 9460 8p7e15 9466 9p7e16 9473 9p8e17 9474 7t7e49 9495 8t7e56 9501 9t7e63 9508 lgsdir2lem3 14324 |
Copyright terms: Public domain | W3C validator |