Definition df-5 8640

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 8632	. 2 class 5
2		c4 8631	. . 3 class 4
3		c1 7501	. . 3 class 1
4		caddc 7503	. . 3 class +
5	2, 3, 4	co 5706	. 2 class ( 4 + 1 )
6	1, 5	wceq 1299	1 wff 5 = ( 4 + 1 )

This definition is referenced by:  5re  8657  5pos  8678  4p1e5  8708  3p2e5  8713  4p2e6  8715  5nn  8736  4lt5  8747  5p5e10  9104  6p5e11  9106  7p5e12  9110  8p5e13  9116  8p7e15  9118  9p5e14  9123  9p6e15  9124  5t5e25  9136  6t5e30  9140  7t5e35  9145  8t5e40  9151  9t5e45  9158  fldiv4p1lem1div2  9919  ef01bndlem  11261  ex-exp  12542  ex-fac  12543  ex-bc  12544