Definition df-5 12242

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 12234	. 2 class 5
2		c4 12233	. . 3 class 4
3		c1 11035	. . 3 class 1
4		caddc 11037	. . 3 class +
5	2, 3, 4	co 7359	. 2 class (4 + 1)
6	1, 5	wceq 1548	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12262  5re  12263  5cn  12264  5pos  12285  5m1e4  12301  4p1e5  12317  3p2e5  12322  4p2e6  12324  4lt5  12348  5p5e10  12710  6p5e11  12712  7p5e12  12716  8p5e13  12722  8p7e15  12724  9p5e14  12729  9p6e15  12730  5t5e25  12742  6t5e30  12746  7t5e35  12751  8t5e40  12757  9t5e45  12764  fldiv4p1lem1div2  13789  ef01bndlem  16146  prm23lt5  16780  5prm  17074  lt6abl  19864  log2ublem3  26933  ppiublem2  27187  bclbnd  27264  bposlem6  27273  bposlem9  27276  lgsdir2lem3  27311  2lgslem3c  27382  2lgsoddprmlem3c  27396  ex-exp  30540  ex-fac  30541  ex-bc  30542  3lexlogpow5ineq5  42558  aks4d1p1p7  42572  rmydioph  43472  expdiophlem2  43480  stoweidlem13  46468  cos5t  47354  fmtno5  48047  fmtnofac1  48060  31prm  48087  5odd  48213  sbgoldbo  48290  gpgprismgr4cycllem7  48604  gpgprismgr4cycllem9  48606  ackval50  49201