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 8934 | . 2 class 7 | |
2 | c6 8933 | . . 3 class 6 | |
3 | c1 7775 | . . 3 class 1 | |
4 | caddc 7777 | . . 3 class + | |
5 | 2, 3, 4 | co 5853 | . 2 class (6 + 1) |
6 | 1, 5 | wceq 1348 | 1 wff 7 = (6 + 1) |
Colors of variables: wff set class |
This definition is referenced by: 7re 8961 7pos 8980 7m1e6 9002 6p1e7 9016 4p3e7 9022 5p2e7 9024 6p2e8 9027 7nn 9044 6lt7 9062 7p7e14 9421 8p7e15 9427 9p7e16 9434 9p8e17 9435 7t7e49 9456 8t7e56 9462 9t7e63 9469 lgsdir2lem3 13725 |
Copyright terms: Public domain | W3C validator |