![]() |
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 11275 | . 2 class 5 | |
2 | c4 11274 | . . 3 class 4 | |
3 | c1 10139 | . . 3 class 1 | |
4 | caddc 10141 | . . 3 class + | |
5 | 2, 3, 4 | co 6793 | . 2 class (4 + 1) |
6 | 1, 5 | wceq 1631 | 1 wff 5 = (4 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 5re 11301 5pos 11320 5m1e4 11341 4p1e5 11356 3p2e5 11362 4p2e6 11364 5p5e10OLD 11370 5nn 11390 4lt5 11402 5p5e10 11797 6p5e11 11801 6p5e11OLD 11802 7p5e12 11808 8p5e13 11816 8p7e15 11818 9p5e14 11824 9p6e15 11825 5t5e25 11840 5t5e25OLD 11841 6t5e30 11845 6t5e30OLD 11846 7t5e35 11852 8t5e40 11858 8t5e40OLD 11859 9t5e45 11867 fldiv4p1lem1div2 12844 ef01bndlem 15120 prm23lt5 15726 5prm 16022 lt6abl 18503 log2ublem3 24896 ppiublem2 25149 bclbnd 25226 bposlem6 25235 bposlem9 25238 lgsdir2lem3 25273 2lgslem3c 25344 2lgsoddprmlem3c 25358 ex-exp 27649 ex-fac 27650 ex-bc 27651 rmydioph 38107 expdiophlem2 38115 stoweidlem13 40747 fmtno5 41997 fmtnofac1 42010 31prm 42040 5odd 42147 sbgoldbo 42203 |
Copyright terms: Public domain | W3C validator |