Definition df-5 12236

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 12228	. 2 class 5
2		c4 12227	. . 3 class 4
3		c1 11028	. . 3 class 1
4		caddc 11030	. . 3 class +
5	2, 3, 4	co 7356	. 2 class (4 + 1)
6	1, 5	wceq 1542	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12256  5re  12257  5cn  12258  5pos  12279  5m1e4  12295  4p1e5  12311  3p2e5  12316  4p2e6  12318  4lt5  12342  5p5e10  12704  6p5e11  12706  7p5e12  12710  8p5e13  12716  8p7e15  12718  9p5e14  12723  9p6e15  12724  5t5e25  12736  6t5e30  12740  7t5e35  12745  8t5e40  12751  9t5e45  12758  fldiv4p1lem1div2  13783  ef01bndlem  16140  prm23lt5  16774  5prm  17068  lt6abl  19859  log2ublem3  26900  ppiublem2  27154  bclbnd  27231  bposlem6  27240  bposlem9  27243  lgsdir2lem3  27278  2lgslem3c  27349  2lgsoddprmlem3c  27363  ex-exp  30508  ex-fac  30509  ex-bc  30510  3lexlogpow5ineq5  42487  aks4d1p1p7  42501  rmydioph  43430  expdiophlem2  43438  stoweidlem13  46429  cos5t  47315  fmtno5  48008  fmtnofac1  48021  31prm  48048  5odd  48174  sbgoldbo  48251  gpgprismgr4cycllem7  48565  gpgprismgr4cycllem9  48567  ackval50  49162