Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-5 | GIF version |
Description: Define the number 5. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-5 | ⊢ 5 = (4 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c5 8742 | . 2 class 5 | |
2 | c4 8741 | . . 3 class 4 | |
3 | c1 7589 | . . 3 class 1 | |
4 | caddc 7591 | . . 3 class + | |
5 | 2, 3, 4 | co 5742 | . 2 class (4 + 1) |
6 | 1, 5 | wceq 1316 | 1 wff 5 = (4 + 1) |
Colors of variables: wff set class |
This definition is referenced by: 5re 8767 5pos 8788 5m1e4 8810 4p1e5 8824 3p2e5 8829 4p2e6 8831 5nn 8852 4lt5 8863 5p5e10 9220 6p5e11 9222 7p5e12 9226 8p5e13 9232 8p7e15 9234 9p5e14 9239 9p6e15 9240 5t5e25 9252 6t5e30 9256 7t5e35 9261 8t5e40 9267 9t5e45 9274 fldiv4p1lem1div2 10046 ef01bndlem 11390 ex-exp 12866 ex-fac 12867 ex-bc 12868 |
Copyright terms: Public domain | W3C validator |