Definition df-5 9375

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 9367	. 2 class 5
2		c4 9366	. . 3 class 4
3		c1 8186	. . 3 class 1
4		caddc 8188	. . 3 class +
5	2, 3, 4	co 6088	. 2 class (4 + 1)
6	1, 5	wceq 1402	1 wff 5 = (4 + 1)

This definition is used by:  5re  9392  5pos  9413  5m1e4  9435  4p1e5  9450  3p2e5  9455  4p2e6  9457  5nn  9480  4lt5  9491  5p5e10  9863  6p5e11  9865  7p5e12  9869  8p5e13  9875  8p7e15  9877  9p5e14  9882  9p6e15  9883  5t5e25  9895  6t5e30  9899  7t5e35  9904  8t5e40  9910  9t5e45  9917  fldiv4p1lem1div2  10761  ef01bndlem  12548  prm23lt5  13071  5prm  13252  log2ublem3  16223  ppiublem2  16292  bclbnd  16307  bposlem6  16316  bposlem9  16319  lgsdir2lem3  16354  2lgslem3c  16419  2lgsoddprmlem3c  16433  ex-exp  16946  ex-fac  16947  ex-bc  16948