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 8919 | . 2 | |
2 | c4 8918 | . . 3 | |
3 | c1 7762 | . . 3 | |
4 | caddc 7764 | . . 3 | |
5 | 2, 3, 4 | co 5850 | . 2 |
6 | 1, 5 | wceq 1348 | 1 |
Colors of variables: wff set class |
This definition is referenced by: 5re 8944 5pos 8965 5m1e4 8987 4p1e5 9001 3p2e5 9006 4p2e6 9008 5nn 9029 4lt5 9040 5p5e10 9400 6p5e11 9402 7p5e12 9406 8p5e13 9412 8p7e15 9414 9p5e14 9419 9p6e15 9420 5t5e25 9432 6t5e30 9436 7t5e35 9441 8t5e40 9447 9t5e45 9454 fldiv4p1lem1div2 10248 ef01bndlem 11706 prm23lt5 12204 lgsdir2lem3 13684 ex-exp 13721 ex-fac 13722 ex-bc 13723 |
Copyright terms: Public domain | W3C validator |