Definition df-5 12275

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 12267	. 2 class 5
2		c4 12266	. . 3 class 4
3		c1 11108	. . 3 class 1
4		caddc 11110	. . 3 class +
5	2, 3, 4	co 7406	. 2 class (4 + 1)
6	1, 5	wceq 1542	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12295  5re  12296  5cn  12297  5pos  12318  5m1e4  12339  4p1e5  12355  3p2e5  12360  4p2e6  12362  4lt5  12386  5p5e10  12745  6p5e11  12747  7p5e12  12751  8p5e13  12757  8p7e15  12759  9p5e14  12764  9p6e15  12765  5t5e25  12777  6t5e30  12781  7t5e35  12786  8t5e40  12792  9t5e45  12799  fldiv4p1lem1div2  13797  ef01bndlem  16124  prm23lt5  16744  5prm  17039  lt6abl  19758  log2ublem3  26443  ppiublem2  26696  bclbnd  26773  bposlem6  26782  bposlem9  26785  lgsdir2lem3  26820  2lgslem3c  26891  2lgsoddprmlem3c  26905  ex-exp  29693  ex-fac  29694  ex-bc  29695  3lexlogpow5ineq5  40914  aks4d1p1p7  40928  rmydioph  41739  expdiophlem2  41747  stoweidlem13  44716  fmtno5  46212  fmtnofac1  46225  31prm  46252  5odd  46365  sbgoldbo  46442  ackval50  47338