Definition df-5 9046

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 9038	. 2 class 5
2		c4 9037	. . 3 class 4
3		c1 7875	. . 3 class 1
4		caddc 7877	. . 3 class +
5	2, 3, 4	co 5919	. 2 class ( 4 + 1 )
6	1, 5	wceq 1364	1 wff 5 = ( 4 + 1 )

This definition is referenced by:  5re  9063  5pos  9084  5m1e4  9106  4p1e5  9121  3p2e5  9126  4p2e6  9128  5nn  9149  4lt5  9160  5p5e10  9521  6p5e11  9523  7p5e12  9527  8p5e13  9533  8p7e15  9535  9p5e14  9540  9p6e15  9541  5t5e25  9553  6t5e30  9557  7t5e35  9562  8t5e40  9568  9t5e45  9575  fldiv4p1lem1div2  10377  ef01bndlem  11902  prm23lt5  12404  lgsdir2lem3  15187  2lgslem3c  15252  2lgsoddprmlem3c  15266  ex-exp  15289  ex-fac  15290  ex-bc  15291