Definition df-5 9301

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 9293	. 2 class 5
2		c4 9292	. . 3 class 4
3		c1 8130	. . 3 class 1
4		caddc 8132	. . 3 class +
5	2, 3, 4	co 6052	. 2 class (4 + 1)
6	1, 5	wceq 1398	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  9318  5pos  9339  5m1e4  9361  4p1e5  9376  3p2e5  9381  4p2e6  9383  5nn  9404  4lt5  9415  5p5e10  9782  6p5e11  9784  7p5e12  9788  8p5e13  9794  8p7e15  9796  9p5e14  9801  9p6e15  9802  5t5e25  9814  6t5e30  9818  7t5e35  9823  8t5e40  9829  9t5e45  9836  fldiv4p1lem1div2  10669  ef01bndlem  12446  prm23lt5  12965  lgsdir2lem3  15920  2lgslem3c  15985  2lgsoddprmlem3c  15999  ex-exp  16512  ex-fac  16513  ex-bc  16514