Definition df-4 9365

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 9357	. 2 class 4
2		c3 9356	. . 3 class 3
3		c1 8180	. . 3 class 1
4		caddc 8182	. . 3 class +
5	2, 3, 4	co 6085	. 2 class ( 3 + 1 )
6	1, 5	wceq 1402	1 wff 4 = ( 3 + 1 )

This definition is used by:  4re  9381  4pos  9401  4m1e3  9425  2p2e4  9431  3p1e4  9440  3p2e5  9446  4p4e8  9450  5p4e9  9453  4nn  9468  3lt4  9477  halfpm6th  9525  6p4e10  9848  7p4e11  9852  7p7e14  9855  8p4e12  9858  8p6e14  9860  9p4e13  9865  9p5e14  9866  4t4e16  9875  5t4e20  9878  6t4e24  9882  7t4e28  9887  8t4e32  9893  9t4e36  9900  fz0to4untppr  10531  fzo0to42pr  10638  4bc2eq6  11213  ef4p  12461  ef01bndlem  12523  sincosq4sgn  15930  binom4  16081  lgsdir2lem3  16149