Definition df-5 9055

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 9047	. 2 class 5
2		c4 9046	. . 3 class 4
3		c1 7883	. . 3 class 1
4		caddc 7885	. . 3 class +
5	2, 3, 4	co 5923	. 2 class ( 4 + 1 )
6	1, 5	wceq 1364	1 wff 5 = ( 4 + 1 )

This definition is referenced by:  5re  9072  5pos  9093  5m1e4  9115  4p1e5  9130  3p2e5  9135  4p2e6  9137  5nn  9158  4lt5  9169  5p5e10  9530  6p5e11  9532  7p5e12  9536  8p5e13  9542  8p7e15  9544  9p5e14  9549  9p6e15  9550  5t5e25  9562  6t5e30  9566  7t5e35  9571  8t5e40  9577  9t5e45  9584  fldiv4p1lem1div2  10398  ef01bndlem  11924  prm23lt5  12443  lgsdir2lem3  15297  2lgslem3c  15362  2lgsoddprmlem3c  15376  ex-exp  15399  ex-fac  15400  ex-bc  15401