Definition df-4 8953

Description: Define the number 4. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
df-4	|- 4 = ( 3 + 1 )

Detailed syntax breakdown of Definition df-4

Step	Hyp	Ref	Expression
1		c4 8945	. 2 class 4
2		c3 8944	. . 3 class 3
3		c1 7787	. . 3 class 1
4		caddc 7789	. . 3 class +
5	2, 3, 4	co 5865	. 2 class ( 3 + 1 )
6	1, 5	wceq 1353	1 wff 4 = ( 3 + 1 )

This definition is referenced by:  4re  8969  4pos  8989  4m1e3  9013  2p2e4  9019  3p1e4  9027  3p2e5  9033  4p4e8  9037  5p4e9  9040  4nn  9055  3lt4  9064  halfpm6th  9112  6p4e10  9428  7p4e11  9432  7p7e14  9435  8p4e12  9438  8p6e14  9440  9p4e13  9445  9p5e14  9446  4t4e16  9455  5t4e20  9458  6t4e24  9462  7t4e28  9467  8t4e32  9473  9t4e36  9480  fz0to4untppr  10094  fzo0to42pr  10190  4bc2eq6  10722  ef4p  11670  ef01bndlem  11732  sincosq4sgn  13830  binom4  13977  lgsdir2lem3  14011