Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-6 | Unicode version |
Description: Define the number 6. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-6 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c6 8743 | . 2 | |
2 | c5 8742 | . . 3 | |
3 | c1 7589 | . . 3 | |
4 | caddc 7591 | . . 3 | |
5 | 2, 3, 4 | co 5742 | . 2 |
6 | 1, 5 | wceq 1316 | 1 |
Colors of variables: wff set class |
This definition is referenced by: 6re 8769 6pos 8789 6m1e5 8811 5p1e6 8825 3p3e6 8830 4p2e6 8831 5p2e7 8834 6nn 8853 5lt6 8867 6p6e12 9223 7p6e13 9227 8p6e14 9233 8p8e16 9235 9p6e15 9240 9p7e16 9241 6t6e36 9257 7t6e42 9262 8t6e48 9268 9t6e54 9275 |
Copyright terms: Public domain | W3C validator |