Definition df-5 11691

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 11683	. 2 class 5
2		c4 11682	. . 3 class 4
3		c1 10527	. . 3 class 1
4		caddc 10529	. . 3 class +
5	2, 3, 4	co 7135	. 2 class (4 + 1)
6	1, 5	wceq 1538	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  11711  5re  11712  5cn  11713  5pos  11734  5m1e4  11755  4p1e5  11771  3p2e5  11776  4p2e6  11778  4lt5  11802  5p5e10  12157  6p5e11  12159  7p5e12  12163  8p5e13  12169  8p7e15  12171  9p5e14  12176  9p6e15  12177  5t5e25  12189  6t5e30  12193  7t5e35  12198  8t5e40  12204  9t5e45  12211  fldiv4p1lem1div2  13200  ef01bndlem  15529  prm23lt5  16141  5prm  16434  lt6abl  19008  log2ublem3  25534  ppiublem2  25787  bclbnd  25864  bposlem6  25873  bposlem9  25876  lgsdir2lem3  25911  2lgslem3c  25982  2lgsoddprmlem3c  25996  ex-exp  28235  ex-fac  28236  ex-bc  28237  rmydioph  39955  expdiophlem2  39963  stoweidlem13  42655  fmtno5  44074  fmtnofac1  44087  31prm  44114  5odd  44228  sbgoldbo  44305  ackval50  45112