![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-7 | Structured version Visualization version GIF version |
Description: Define the number 7. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-7 | ⊢ 7 = (6 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c7 12316 | . 2 class 7 | |
2 | c6 12315 | . . 3 class 6 | |
3 | c1 11148 | . . 3 class 1 | |
4 | caddc 11150 | . . 3 class + | |
5 | 2, 3, 4 | co 7414 | . 2 class (6 + 1) |
6 | 1, 5 | wceq 1534 | 1 wff 7 = (6 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 7nn 12348 7re 12349 7cn 12350 7pos 12367 7m1e6 12388 6p1e7 12404 4p3e7 12410 5p2e7 12412 6p2e8 12415 6lt7 12442 7p7e14 12800 8p7e15 12806 9p7e16 12813 9p8e17 12814 7t7e49 12835 8t7e56 12841 9t7e63 12848 2exp7 17083 7prm 17106 17prm 17112 37prm 17116 317prm 17121 log2ublem2 26970 log2ublem3 26971 bclbnd 27304 bposlem8 27315 lgsdir2lem3 27351 problem4 35507 3cubeslem3r 42379 rmydioph 42707 expdiophlem2 42715 fmtno5 47163 257prm 47167 127prm 47205 7odd 47318 stgoldbwt 47382 |
Copyright terms: Public domain | W3C validator |