Definition df-4 9051

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 9043	. 2 class 4
2		c3 9042	. . 3 class 3
3		c1 7880	. . 3 class 1
4		caddc 7882	. . 3 class +
5	2, 3, 4	co 5922	. 2 class ( 3 + 1 )
6	1, 5	wceq 1364	1 wff 4 = ( 3 + 1 )

This definition is referenced by:  4re  9067  4pos  9087  4m1e3  9111  2p2e4  9117  3p1e4  9126  3p2e5  9132  4p4e8  9136  5p4e9  9139  4nn  9154  3lt4  9163  halfpm6th  9211  6p4e10  9528  7p4e11  9532  7p7e14  9535  8p4e12  9538  8p6e14  9540  9p4e13  9545  9p5e14  9546  4t4e16  9555  5t4e20  9558  6t4e24  9562  7t4e28  9567  8t4e32  9573  9t4e36  9580  fz0to4untppr  10199  fzo0to42pr  10296  4bc2eq6  10866  ef4p  11859  ef01bndlem  11921  sincosq4sgn  15065  binom4  15215  lgsdir2lem3  15271