Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-7 | Unicode version |
Description: Define the number 7. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-7 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c7 8904 | . 2 | |
2 | c6 8903 | . . 3 | |
3 | c1 7745 | . . 3 | |
4 | caddc 7747 | . . 3 | |
5 | 2, 3, 4 | co 5836 | . 2 |
6 | 1, 5 | wceq 1342 | 1 |
Colors of variables: wff set class |
This definition is referenced by: 7re 8931 7pos 8950 7m1e6 8972 6p1e7 8986 4p3e7 8992 5p2e7 8994 6p2e8 8997 7nn 9014 6lt7 9032 7p7e14 9391 8p7e15 9397 9p7e16 9404 9p8e17 9405 7t7e49 9426 8t7e56 9432 9t7e63 9439 |
Copyright terms: Public domain | W3C validator |