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 11684 | . 2 class 5 | |
2 | c4 11683 | . . 3 class 4 | |
3 | c1 10527 | . . 3 class 1 | |
4 | caddc 10529 | . . 3 class + | |
5 | 2, 3, 4 | co 7145 | . 2 class (4 + 1) |
6 | 1, 5 | wceq 1528 | 1 wff 5 = (4 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 5nn 11712 5re 11713 5cn 11714 5pos 11735 5m1e4 11756 4p1e5 11772 3p2e5 11777 4p2e6 11779 4lt5 11803 5p5e10 12158 6p5e11 12160 7p5e12 12164 8p5e13 12170 8p7e15 12172 9p5e14 12177 9p6e15 12178 5t5e25 12190 6t5e30 12194 7t5e35 12199 8t5e40 12205 9t5e45 12212 fldiv4p1lem1div2 13195 ef01bndlem 15527 prm23lt5 16141 5prm 16432 lt6abl 18946 log2ublem3 25454 ppiublem2 25707 bclbnd 25784 bposlem6 25793 bposlem9 25796 lgsdir2lem3 25831 2lgslem3c 25902 2lgsoddprmlem3c 25916 ex-exp 28157 ex-fac 28158 ex-bc 28159 rmydioph 39491 expdiophlem2 39499 stoweidlem13 42179 fmtno5 43566 fmtnofac1 43579 31prm 43607 5odd 43722 sbgoldbo 43799 |
Copyright terms: Public domain | W3C validator |