Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-5 | Unicode version |
Description: Define the number 5. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-5 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c5 8092 | . 2 | |
2 | c4 8091 | . . 3 | |
3 | c1 6982 | . . 3 | |
4 | caddc 6984 | . . 3 | |
5 | 2, 3, 4 | co 5532 | . 2 |
6 | 1, 5 | wceq 1284 | 1 |
Colors of variables: wff set class |
This definition is referenced by: 5re 8118 5pos 8139 4p1e5 8168 3p2e5 8173 4p2e6 8175 5nn 8196 4lt5 8207 5p5e10 8547 6p5e11 8549 7p5e12 8553 8p5e13 8559 8p7e15 8561 9p5e14 8566 9p6e15 8567 5t5e25 8579 6t5e30 8583 7t5e35 8588 8t5e40 8594 9t5e45 8601 fldiv4p1lem1div2 9307 ex-fac 10565 ex-bc 10566 |
Copyright terms: Public domain | W3C validator |