Definition df-5 9348

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 9340	. 2 class 5
2		c4 9339	. . 3 class 4
3		c1 8173	. . 3 class 1
4		caddc 8175	. . 3 class +
5	2, 3, 4	co 6078	. 2 class ( 4 + 1 )
6	1, 5	wceq 1402	1 wff 5 = ( 4 + 1 )

This definition is referenced by:  5re  9365  5pos  9386  5m1e4  9408  4p1e5  9423  3p2e5  9428  4p2e6  9430  5nn  9451  4lt5  9462  5p5e10  9829  6p5e11  9831  7p5e12  9835  8p5e13  9841  8p7e15  9843  9p5e14  9848  9p6e15  9849  5t5e25  9861  6t5e30  9865  7t5e35  9870  8t5e40  9876  9t5e45  9883  fldiv4p1lem1div2  10721  ef01bndlem  12504  prm23lt5  13023  lgsdir2lem3  16066  2lgslem3c  16131  2lgsoddprmlem3c  16145  ex-exp  16658  ex-fac  16659  ex-bc  16660