Definition df-5 12278

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 12270	. 2 class 5
2		c4 12269	. . 3 class 4
3		c1 11111	. . 3 class 1
4		caddc 11113	. . 3 class +
5	2, 3, 4	co 7409	. 2 class (4 + 1)
6	1, 5	wceq 1542	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12298  5re  12299  5cn  12300  5pos  12321  5m1e4  12342  4p1e5  12358  3p2e5  12363  4p2e6  12365  4lt5  12389  5p5e10  12748  6p5e11  12750  7p5e12  12754  8p5e13  12760  8p7e15  12762  9p5e14  12767  9p6e15  12768  5t5e25  12780  6t5e30  12784  7t5e35  12789  8t5e40  12795  9t5e45  12802  fldiv4p1lem1div2  13800  ef01bndlem  16127  prm23lt5  16747  5prm  17042  lt6abl  19763  log2ublem3  26453  ppiublem2  26706  bclbnd  26783  bposlem6  26792  bposlem9  26795  lgsdir2lem3  26830  2lgslem3c  26901  2lgsoddprmlem3c  26915  ex-exp  29703  ex-fac  29704  ex-bc  29705  3lexlogpow5ineq5  40925  aks4d1p1p7  40939  rmydioph  41753  expdiophlem2  41761  stoweidlem13  44729  fmtno5  46225  fmtnofac1  46238  31prm  46265  5odd  46378  sbgoldbo  46455  ackval50  47384