Definition df-5 8983

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 8975	. 2 class 5
2		c4 8974	. . 3 class 4
3		c1 7814	. . 3 class 1
4		caddc 7816	. . 3 class +
5	2, 3, 4	co 5877	. 2 class (4 + 1)
6	1, 5	wceq 1353	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  9000  5pos  9021  5m1e4  9043  4p1e5  9057  3p2e5  9062  4p2e6  9064  5nn  9085  4lt5  9096  5p5e10  9456  6p5e11  9458  7p5e12  9462  8p5e13  9468  8p7e15  9470  9p5e14  9475  9p6e15  9476  5t5e25  9488  6t5e30  9492  7t5e35  9497  8t5e40  9503  9t5e45  9510  fldiv4p1lem1div2  10307  ef01bndlem  11766  prm23lt5  12265  lgsdir2lem3  14516  2lgsoddprmlem3c  14542  ex-exp  14564  ex-fac  14565  ex-bc  14566