Definition df-5 8940

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 8932	. 2 class 5
2		c4 8931	. . 3 class 4
3		c1 7775	. . 3 class 1
4		caddc 7777	. . 3 class +
5	2, 3, 4	co 5853	. 2 class ( 4 + 1 )
6	1, 5	wceq 1348	1 wff 5 = ( 4 + 1 )

This definition is referenced by:  5re  8957  5pos  8978  5m1e4  9000  4p1e5  9014  3p2e5  9019  4p2e6  9021  5nn  9042  4lt5  9053  5p5e10  9413  6p5e11  9415  7p5e12  9419  8p5e13  9425  8p7e15  9427  9p5e14  9432  9p6e15  9433  5t5e25  9445  6t5e30  9449  7t5e35  9454  8t5e40  9460  9t5e45  9467  fldiv4p1lem1div2  10261  ef01bndlem  11719  prm23lt5  12217  lgsdir2lem3  13725  ex-exp  13762  ex-fac  13763  ex-bc  13764