Definition df-5 8927

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 8919	. 2 class 5
2		c4 8918	. . 3 class 4
3		c1 7762	. . 3 class 1
4		caddc 7764	. . 3 class +
5	2, 3, 4	co 5850	. 2 class ( 4 + 1 )
6	1, 5	wceq 1348	1 wff 5 = ( 4 + 1 )

This definition is referenced by:  5re  8944  5pos  8965  5m1e4  8987  4p1e5  9001  3p2e5  9006  4p2e6  9008  5nn  9029  4lt5  9040  5p5e10  9400  6p5e11  9402  7p5e12  9406  8p5e13  9412  8p7e15  9414  9p5e14  9419  9p6e15  9420  5t5e25  9432  6t5e30  9436  7t5e35  9441  8t5e40  9447  9t5e45  9454  fldiv4p1lem1div2  10248  ef01bndlem  11706  prm23lt5  12204  lgsdir2lem3  13684  ex-exp  13721  ex-fac  13722  ex-bc  13723