Definition df-5 9366

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 9358	. 2 class 5
2		c4 9357	. . 3 class 4
3		c1 8180	. . 3 class 1
4		caddc 8182	. . 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  9383  5pos  9404  5m1e4  9426  4p1e5  9441  3p2e5  9446  4p2e6  9448  5nn  9469  4lt5  9480  5p5e10  9847  6p5e11  9849  7p5e12  9853  8p5e13  9859  8p7e15  9861  9p5e14  9866  9p6e15  9867  5t5e25  9879  6t5e30  9883  7t5e35  9888  8t5e40  9894  9t5e45  9901  fldiv4p1lem1div2  10740  ef01bndlem  12523  prm23lt5  13042  log2ublem3  16085  lgsdir2lem3  16149  2lgslem3c  16214  2lgsoddprmlem3c  16228  ex-exp  16741  ex-fac  16742  ex-bc  16743