Definition df-5 8981

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 8973	. 2 class 5
2		c4 8972	. . 3 class 4
3		c1 7812	. . 3 class 1
4		caddc 7814	. . 3 class +
5	2, 3, 4	co 5875	. 2 class ( 4 + 1 )
6	1, 5	wceq 1353	1 wff 5 = ( 4 + 1 )

This definition is referenced by:  5re  8998  5pos  9019  5m1e4  9041  4p1e5  9055  3p2e5  9060  4p2e6  9062  5nn  9083  4lt5  9094  5p5e10  9454  6p5e11  9456  7p5e12  9460  8p5e13  9466  8p7e15  9468  9p5e14  9473  9p6e15  9474  5t5e25  9486  6t5e30  9490  7t5e35  9495  8t5e40  9501  9t5e45  9508  fldiv4p1lem1div2  10305  ef01bndlem  11764  prm23lt5  12263  lgsdir2lem3  14434  2lgsoddprmlem3c  14460  ex-exp  14482  ex-fac  14483  ex-bc  14484