![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE 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 10615 | . 2 | |
2 | c6 10614 | . . 3 | |
3 | c1 9514 | . . 3 | |
4 | caddc 9516 | . . 3 | |
5 | 2, 3, 4 | co 6296 | . 2 |
6 | 1, 5 | wceq 1395 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: 7re 10643 7pos 10660 6p1e7 10689 4p3e7 10696 5p2e7 10698 6p2e8 10702 7nn 10723 6lt7 10742 7p7e14 11059 8p7e15 11064 9p7e16 11071 9p8e17 11072 7t7e49 11091 8t7e56 11097 9t7e63 11104 7prm 14596 17prm 14602 37prm 14606 317prm 14611 log2ublem2 23278 log2ublem3 23279 bclbnd 23555 bposlem8 23566 lgsdir2lem3 23600 problem4 29022 rmydioph 30956 expdiophlem2 30964 |
Copyright terms: Public domain | W3C validator |