Definition df-5 12359

Description: Define the number 5. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
df-5	⊢ 5 = (4 + 1)

Detailed syntax breakdown of Definition df-5

Step	Hyp	Ref	Expression
1		c5 12351	. 2 class 5
2		c4 12350	. . 3 class 4
3		c1 11185	. . 3 class 1
4		caddc 11187	. . 3 class +
5	2, 3, 4	co 7448	. 2 class (4 + 1)
6	1, 5	wceq 1537	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12379  5re  12380  5cn  12381  5pos  12402  5m1e4  12423  4p1e5  12439  3p2e5  12444  4p2e6  12446  4lt5  12470  5p5e10  12829  6p5e11  12831  7p5e12  12835  8p5e13  12841  8p7e15  12843  9p5e14  12848  9p6e15  12849  5t5e25  12861  6t5e30  12865  7t5e35  12870  8t5e40  12876  9t5e45  12883  fldiv4p1lem1div2  13886  ef01bndlem  16232  prm23lt5  16861  5prm  17156  lt6abl  19937  log2ublem3  27009  ppiublem2  27265  bclbnd  27342  bposlem6  27351  bposlem9  27354  lgsdir2lem3  27389  2lgslem3c  27460  2lgsoddprmlem3c  27474  ex-exp  30482  ex-fac  30483  ex-bc  30484  3lexlogpow5ineq5  42017  aks4d1p1p7  42031  rmydioph  42971  expdiophlem2  42979  stoweidlem13  45934  fmtno5  47431  fmtnofac1  47444  31prm  47471  5odd  47584  sbgoldbo  47661  ackval50  48432