Definition df-5 8168

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 8159	. 2 class 5
2		c4 8158	. . 3 class 4
3		c1 7044	. . 3 class 1
4		caddc 7046	. . 3 class +
5	2, 3, 4	co 5543	. 2 class (4 + 1)
6	1, 5	wceq 1285	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  8185  5pos  8206  4p1e5  8235  3p2e5  8240  4p2e6  8242  5nn  8263  4lt5  8274  5p5e10  8628  6p5e11  8630  7p5e12  8634  8p5e13  8640  8p7e15  8642  9p5e14  8647  9p6e15  8648  5t5e25  8660  6t5e30  8664  7t5e35  8669  8t5e40  8675  9t5e45  8682  fldiv4p1lem1div2  9387  ex-fac  10716  ex-bc  10717