Definition df-5 8919

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 8911	. 2 class 5
2		c4 8910	. . 3 class 4
3		c1 7754	. . 3 class 1
4		caddc 7756	. . 3 class +
5	2, 3, 4	co 5842	. 2 class ( 4 + 1 )
6	1, 5	wceq 1343	1 wff 5 = ( 4 + 1 )

This definition is referenced by:  5re  8936  5pos  8957  5m1e4  8979  4p1e5  8993  3p2e5  8998  4p2e6  9000  5nn  9021  4lt5  9032  5p5e10  9392  6p5e11  9394  7p5e12  9398  8p5e13  9404  8p7e15  9406  9p5e14  9411  9p6e15  9412  5t5e25  9424  6t5e30  9428  7t5e35  9433  8t5e40  9439  9t5e45  9446  fldiv4p1lem1div2  10240  ef01bndlem  11697  prm23lt5  12195  lgsdir2lem3  13571  ex-exp  13608  ex-fac  13609  ex-bc  13610