Definition df-4 8980

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 8972	. 2 class 4
2		c3 8971	. . 3 class 3
3		c1 7812	. . 3 class 1
4		caddc 7814	. . 3 class +
5	2, 3, 4	co 5875	. 2 class ( 3 + 1 )
6	1, 5	wceq 1353	1 wff 4 = ( 3 + 1 )

This definition is referenced by:  4re  8996  4pos  9016  4m1e3  9040  2p2e4  9046  3p1e4  9054  3p2e5  9060  4p4e8  9064  5p4e9  9067  4nn  9082  3lt4  9091  halfpm6th  9139  6p4e10  9455  7p4e11  9459  7p7e14  9462  8p4e12  9465  8p6e14  9467  9p4e13  9472  9p5e14  9473  4t4e16  9482  5t4e20  9485  6t4e24  9489  7t4e28  9494  8t4e32  9500  9t4e36  9507  fz0to4untppr  10124  fzo0to42pr  10220  4bc2eq6  10754  ef4p  11702  ef01bndlem  11764  sincosq4sgn  14253  binom4  14400  lgsdir2lem3  14434