Definition df-5 9369

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 9361	. 2 class 5
2		c4 9360	. . 3 class 4
3		c1 8181	. . 3 class 1
4		caddc 8183	. . 3 class +
5	2, 3, 4	co 6085	. 2 class ( 4 + 1 )
6	1, 5	wceq 1402	1 wff 5 = ( 4 + 1 )

This definition is used by:  5re  9386  5pos  9407  5m1e4  9429  4p1e5  9444  3p2e5  9449  4p2e6  9451  5nn  9474  4lt5  9485  5p5e10  9857  6p5e11  9859  7p5e12  9863  8p5e13  9869  8p7e15  9871  9p5e14  9876  9p6e15  9877  5t5e25  9889  6t5e30  9893  7t5e35  9898  8t5e40  9904  9t5e45  9911  fldiv4p1lem1div2  10755  ef01bndlem  12542  prm23lt5  13065  5prm  13246  log2ublem3  16197  ppiublem2  16266  bclbnd  16281  bposlem6  16290  bposlem9  16293  lgsdir2lem3  16328  2lgslem3c  16393  2lgsoddprmlem3c  16407  ex-exp  16920  ex-fac  16921  ex-bc  16922