Definition df-4 8939

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 8931	. 2 class 4
2		c3 8930	. . 3 class 3
3		c1 7775	. . 3 class 1
4		caddc 7777	. . 3 class +
5	2, 3, 4	co 5853	. 2 class ( 3 + 1 )
6	1, 5	wceq 1348	1 wff 4 = ( 3 + 1 )

This definition is referenced by:  4re  8955  4pos  8975  4m1e3  8999  2p2e4  9005  3p1e4  9013  3p2e5  9019  4p4e8  9023  5p4e9  9026  4nn  9041  3lt4  9050  halfpm6th  9098  6p4e10  9414  7p4e11  9418  7p7e14  9421  8p4e12  9424  8p6e14  9426  9p4e13  9431  9p5e14  9432  4t4e16  9441  5t4e20  9444  6t4e24  9448  7t4e28  9453  8t4e32  9459  9t4e36  9466  fz0to4untppr  10080  fzo0to42pr  10176  4bc2eq6  10708  ef4p  11657  ef01bndlem  11719  sincosq4sgn  13544  binom4  13691  lgsdir2lem3  13725