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  9862  6p5e11  9864  7p5e12  9868  8p5e13  9874  8p7e15  9876  9p5e14  9881  9p6e15  9882  5t5e25  9894  6t5e30  9898  7t5e35  9903  8t5e40  9909  9t5e45  9916  fldiv4p1lem1div2  10760  ef01bndlem  12547  prm23lt5  13070  5prm  13251  log2ublem3  16240  ppiublem2  16309  bclbnd  16324  bposlem6  16333  bposlem9  16336  lgsdir2lem3  16371  2lgslem3c  16436  2lgsoddprmlem3c  16450  ex-exp  16963  ex-fac  16964  ex-bc  16965