Definition df-5 7976

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 7967	. 2 class 5
2		c4 7966	. . 3 class 4
3		c1 6890	. . 3 class 1
4		caddc 6892	. . 3 class +
5	2, 3, 4	co 5512	. 2 class (4 + 1)
6	1, 5	wceq 1243	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  7994  5pos  8016  4p1e5  8046  3p2e5  8052  4p2e6  8054  5p5e10  8060  5nn  8080  4lt5  8092  6p5e11  8417  7p5e12  8420  8p5e13  8425  8p7e15  8427  9p5e14  8432  9p6e15  8433  5t5e25  8443  6t5e30  8447  7t5e35  8452  8t5e40  8458  9t5e45  8465  fldiv4p1lem1div2  9147