Definition df-5 9264

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 9256	. 2 class 5
2		c4 9255	. . 3 class 4
3		c1 8093	. . 3 class 1
4		caddc 8095	. . 3 class +
5	2, 3, 4	co 6028	. 2 class (4 + 1)
6	1, 5	wceq 1398	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  9281  5pos  9302  5m1e4  9324  4p1e5  9339  3p2e5  9344  4p2e6  9346  5nn  9367  4lt5  9378  5p5e10  9742  6p5e11  9744  7p5e12  9748  8p5e13  9754  8p7e15  9756  9p5e14  9761  9p6e15  9762  5t5e25  9774  6t5e30  9778  7t5e35  9783  8t5e40  9789  9t5e45  9796  fldiv4p1lem1div2  10628  ef01bndlem  12397  prm23lt5  12916  lgsdir2lem3  15849  2lgslem3c  15914  2lgsoddprmlem3c  15928  ex-exp  16441  ex-fac  16442  ex-bc  16443