Definition df-5 9195

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 9187	. 2 class 5
2		c4 9186	. . 3 class 4
3		c1 8023	. . 3 class 1
4		caddc 8025	. . 3 class +
5	2, 3, 4	co 6013	. 2 class (4 + 1)
6	1, 5	wceq 1395	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  9212  5pos  9233  5m1e4  9255  4p1e5  9270  3p2e5  9275  4p2e6  9277  5nn  9298  4lt5  9309  5p5e10  9671  6p5e11  9673  7p5e12  9677  8p5e13  9683  8p7e15  9685  9p5e14  9690  9p6e15  9691  5t5e25  9703  6t5e30  9707  7t5e35  9712  8t5e40  9718  9t5e45  9725  fldiv4p1lem1div2  10555  ef01bndlem  12307  prm23lt5  12826  lgsdir2lem3  15749  2lgslem3c  15814  2lgsoddprmlem3c  15828  ex-exp  16259  ex-fac  16260  ex-bc  16261