Definition df-5 12377

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 12369	. 2 class 5
2		c4 12368	. . 3 class 4
3		c1 11172	. . 3 class 1
4		caddc 11174	. . 3 class +
5	2, 3, 4	co 7408	. 2 class (4 + 1)
6	1, 5	wceq 1570	1 wff 5 = (4 + 1)

This definition is used by:  5nn  12398  5re  12399  5cn  12400  5m1e4  12441  4p1e5  12457  3p2e5  12462  4p2e6  12464  4lt5  12491  5p5e10  12859  6p5e11  12861  7p5e12  12865  8p5e13  12871  8p7e15  12873  9p5e14  12878  9p6e15  12879  5t5e25  12891  6t5e30  12895  7t5e35  12900  8t5e40  12906  9t5e45  12913  fldiv4p1lem1div2  13943  ef01bndlem  16319  prm23lt5  16953  5prm  17247  lt6abl  20070  log2ublem3  27239  ppiublem2  27493  bclbnd  27570  bposlem6  27579  bposlem9  27582  lgsdir2lem3  27617  2lgslem3c  27688  2lgsoddprmlem3c  27702  ex-exp  30984  ex-fac  30985  ex-bc  30986  3lexlogpow5ineq5  43030  aks4d1p1p7  43044  1p5e6  43232  4p5e9  43244  rmydioph  43959  expdiophlem2  43967  stoweidlem13  46945  cos5t  47847  goldpolyfactor  47849  goldratval  47858  fmtno5  48564  fmtnofac1  48577  31prm  48604  5odd  48730  sbgoldbo  48807  gpgprismgr4cycllem7  49121  gpgprismgr4cycllem9  49123  ackval50  49732