Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-5 | Structured version Visualization version 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 10950 | . 2 class 5 | |
2 | c4 10949 | . . 3 class 4 | |
3 | c1 9816 | . . 3 class 1 | |
4 | caddc 9818 | . . 3 class + | |
5 | 2, 3, 4 | co 6549 | . 2 class (4 + 1) |
6 | 1, 5 | wceq 1475 | 1 wff 5 = (4 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 5re 10976 5pos 10995 5m1e4 11016 4p1e5 11031 3p2e5 11037 4p2e6 11039 5p5e10OLD 11045 5nn 11065 4lt5 11077 5p5e10 11472 6p5e11 11476 6p5e11OLD 11477 7p5e12 11483 8p5e13 11491 8p7e15 11493 9p5e14 11499 9p6e15 11500 5t5e25 11515 5t5e25OLD 11516 6t5e30 11520 6t5e30OLD 11521 7t5e35 11527 8t5e40 11533 8t5e40OLD 11534 9t5e45 11542 fldiv4p1lem1div2 12498 ef01bndlem 14753 prm23lt5 15357 5prm 15653 lt6abl 18119 log2ublem3 24475 ppiublem2 24728 bclbnd 24805 bposlem6 24814 bposlem9 24817 lgsdir2lem3 24852 2lgslem3c 24923 2lgsoddprmlem3c 24937 ex-exp 26699 ex-fac 26700 ex-bc 26701 rmydioph 36599 expdiophlem2 36607 stoweidlem13 38906 fmtno5 40007 fmtnofac1 40020 31prm 40050 5odd 40157 |
Copyright terms: Public domain | W3C validator |