Definition df-4 9286

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 9278	. 2 class 4
2		c3 9277	. . 3 class 3
3		c1 8116	. . 3 class 1
4		caddc 8118	. . 3 class +
5	2, 3, 4	co 6041	. 2 class ( 3 + 1 )
6	1, 5	wceq 1398	1 wff 4 = ( 3 + 1 )

This definition is referenced by:  4re  9302  4pos  9322  4m1e3  9346  2p2e4  9352  3p1e4  9361  3p2e5  9367  4p4e8  9371  5p4e9  9374  4nn  9389  3lt4  9398  halfpm6th  9446  6p4e10  9766  7p4e11  9770  7p7e14  9773  8p4e12  9776  8p6e14  9778  9p4e13  9783  9p5e14  9784  4t4e16  9793  5t4e20  9796  6t4e24  9800  7t4e28  9805  8t4e32  9811  9t4e36  9818  fz0to4untppr  10444  fzo0to42pr  10551  4bc2eq6  11122  ef4p  12358  ef01bndlem  12420  sincosq4sgn  15664  binom4  15814  lgsdir2lem3  15873