Definition df-5 12244

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 12236	. 2 class 5
2		c4 12235	. . 3 class 4
3		c1 11036	. . 3 class 1
4		caddc 11038	. . 3 class +
5	2, 3, 4	co 7364	. 2 class (4 + 1)
6	1, 5	wceq 1542	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12264  5re  12265  5cn  12266  5pos  12287  5m1e4  12303  4p1e5  12319  3p2e5  12324  4p2e6  12326  4lt5  12350  5p5e10  12712  6p5e11  12714  7p5e12  12718  8p5e13  12724  8p7e15  12726  9p5e14  12731  9p6e15  12732  5t5e25  12744  6t5e30  12748  7t5e35  12753  8t5e40  12759  9t5e45  12766  fldiv4p1lem1div2  13791  ef01bndlem  16148  prm23lt5  16782  5prm  17076  lt6abl  19867  log2ublem3  26909  ppiublem2  27163  bclbnd  27240  bposlem6  27249  bposlem9  27252  lgsdir2lem3  27287  2lgslem3c  27358  2lgsoddprmlem3c  27372  ex-exp  30517  ex-fac  30518  ex-bc  30519  3lexlogpow5ineq5  42496  aks4d1p1p7  42510  rmydioph  43439  expdiophlem2  43447  stoweidlem13  46438  fmtno5  48011  fmtnofac1  48024  31prm  48051  5odd  48177  sbgoldbo  48254  gpgprismgr4cycllem7  48568  gpgprismgr4cycllem9  48570  ackval50  49165