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 11034	. . 3 class 1
4		caddc 11036	. . 3 class +
5	2, 3, 4	co 7360	. 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  19865  log2ublem3  26934  ppiublem2  27188  bclbnd  27265  bposlem6  27274  bposlem9  27277  lgsdir2lem3  27312  2lgslem3c  27383  2lgsoddprmlem3c  27397  ex-exp  30542  ex-fac  30543  ex-bc  30544  3lexlogpow5ineq5  42560  aks4d1p1p7  42574  rmydioph  43474  expdiophlem2  43482  stoweidlem13  46470  cos5t  47356  fmtno5  48049  fmtnofac1  48062  31prm  48089  5odd  48215  sbgoldbo  48292  gpgprismgr4cycllem7  48606  gpgprismgr4cycllem9  48608  ackval50  49203