Definition df-5 12022

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 12014	. 2 class 5
2		c4 12013	. . 3 class 4
3		c1 10856	. . 3 class 1
4		caddc 10858	. . 3 class +
5	2, 3, 4	co 7268	. 2 class (4 + 1)
6	1, 5	wceq 1541	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12042  5re  12043  5cn  12044  5pos  12065  5m1e4  12086  4p1e5  12102  3p2e5  12107  4p2e6  12109  4lt5  12133  5p5e10  12490  6p5e11  12492  7p5e12  12496  8p5e13  12502  8p7e15  12504  9p5e14  12509  9p6e15  12510  5t5e25  12522  6t5e30  12526  7t5e35  12531  8t5e40  12537  9t5e45  12544  fldiv4p1lem1div2  13536  ef01bndlem  15874  prm23lt5  16496  5prm  16791  lt6abl  19477  log2ublem3  26079  ppiublem2  26332  bclbnd  26409  bposlem6  26418  bposlem9  26421  lgsdir2lem3  26456  2lgslem3c  26527  2lgsoddprmlem3c  26541  ex-exp  28793  ex-fac  28794  ex-bc  28795  3lexlogpow5ineq5  40048  aks4d1p1p7  40062  rmydioph  40816  expdiophlem2  40824  stoweidlem13  43508  fmtno5  44961  fmtnofac1  44974  31prm  45001  5odd  45114  sbgoldbo  45191  ackval50  45996