Definition df-5 9168

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 9160	. 2 class 5
2		c4 9159	. . 3 class 4
3		c1 7996	. . 3 class 1
4		caddc 7998	. . 3 class +
5	2, 3, 4	co 6000	. 2 class (4 + 1)
6	1, 5	wceq 1395	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  9185  5pos  9206  5m1e4  9228  4p1e5  9243  3p2e5  9248  4p2e6  9250  5nn  9271  4lt5  9282  5p5e10  9644  6p5e11  9646  7p5e12  9650  8p5e13  9656  8p7e15  9658  9p5e14  9663  9p6e15  9664  5t5e25  9676  6t5e30  9680  7t5e35  9685  8t5e40  9691  9t5e45  9698  fldiv4p1lem1div2  10520  ef01bndlem  12262  prm23lt5  12781  lgsdir2lem3  15703  2lgslem3c  15768  2lgsoddprmlem3c  15782  ex-exp  16049  ex-fac  16050  ex-bc  16051