Definition df-4 9045

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

This definition is referenced by:  4re  9061  4pos  9081  4m1e3  9105  2p2e4  9111  3p1e4  9120  3p2e5  9126  4p4e8  9130  5p4e9  9133  4nn  9148  3lt4  9157  halfpm6th  9205  6p4e10  9522  7p4e11  9526  7p7e14  9529  8p4e12  9532  8p6e14  9534  9p4e13  9539  9p5e14  9540  4t4e16  9549  5t4e20  9552  6t4e24  9556  7t4e28  9561  8t4e32  9567  9t4e36  9574  fz0to4untppr  10193  fzo0to42pr  10290  4bc2eq6  10848  ef4p  11840  ef01bndlem  11902  sincosq4sgn  15005  binom4  15152  lgsdir2lem3  15187