Definition df-5 8775

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 8767	. 2 class 5
2		c4 8766	. . 3 class 4
3		c1 7614	. . 3 class 1
4		caddc 7616	. . 3 class +
5	2, 3, 4	co 5767	. 2 class ( 4 + 1 )
6	1, 5	wceq 1331	1 wff 5 = ( 4 + 1 )

This definition is referenced by:  5re  8792  5pos  8813  5m1e4  8835  4p1e5  8849  3p2e5  8854  4p2e6  8856  5nn  8877  4lt5  8888  5p5e10  9245  6p5e11  9247  7p5e12  9251  8p5e13  9257  8p7e15  9259  9p5e14  9264  9p6e15  9265  5t5e25  9277  6t5e30  9281  7t5e35  9286  8t5e40  9292  9t5e45  9299  fldiv4p1lem1div2  10071  ef01bndlem  11452  ex-exp  12928  ex-fac  12929  ex-bc  12930