Definition df-5 8412

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 8403	. 2 class 5
2		c4 8402	. . 3 class 4
3		c1 7288	. . 3 class 1
4		caddc 7290	. . 3 class +
5	2, 3, 4	co 5607	. 2 class ( 4 + 1 )
6	1, 5	wceq 1287	1 wff 5 = ( 4 + 1 )

This definition is referenced by:  5re  8429  5pos  8450  4p1e5  8479  3p2e5  8484  4p2e6  8486  5nn  8507  4lt5  8518  5p5e10  8872  6p5e11  8874  7p5e12  8878  8p5e13  8884  8p7e15  8886  9p5e14  8891  9p6e15  8892  5t5e25  8904  6t5e30  8908  7t5e35  8913  8t5e40  8919  9t5e45  8926  fldiv4p1lem1div2  9633  ex-fac  11085  ex-bc  11086