Definition df-5 9006

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 8998	. 2 class 5
2		c4 8997	. . 3 class 4
3		c1 7837	. . 3 class 1
4		caddc 7839	. . 3 class +
5	2, 3, 4	co 5892	. 2 class ( 4 + 1 )
6	1, 5	wceq 1364	1 wff 5 = ( 4 + 1 )

This definition is referenced by:  5re  9023  5pos  9044  5m1e4  9066  4p1e5  9080  3p2e5  9085  4p2e6  9087  5nn  9108  4lt5  9119  5p5e10  9479  6p5e11  9481  7p5e12  9485  8p5e13  9491  8p7e15  9493  9p5e14  9498  9p6e15  9499  5t5e25  9511  6t5e30  9515  7t5e35  9520  8t5e40  9526  9t5e45  9533  fldiv4p1lem1div2  10331  ef01bndlem  11791  prm23lt5  12290  lgsdir2lem3  14868  2lgsoddprmlem3c  14894  ex-exp  14916  ex-fac  14917  ex-bc  14918