Definition df-4 9374

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 9366	. 2 class 4
2		c3 9365	. . 3 class 3
3		c1 8186	. . 3 class 1
4		caddc 8188	. . 3 class +
5	2, 3, 4	co 6088	. 2 class ( 3 + 1 )
6	1, 5	wceq 1402	1 wff 4 = ( 3 + 1 )

This definition is used by:  4re  9390  4pos  9410  4m1e3  9434  2p2e4  9440  3p1e4  9449  3p2e5  9455  4p4e8  9459  5p4e9  9462  4nn  9479  3lt4  9488  halfpm6th  9536  6p4e10  9864  7p4e11  9868  7p7e14  9871  8p4e12  9874  8p6e14  9876  9p4e13  9881  9p5e14  9882  4t4e16  9891  5t4e20  9894  6t4e24  9898  7t4e28  9903  8t4e32  9909  9t4e36  9916  fz0to4untppr  10548  fzo0to42pr  10655  4bc2eq6  11235  ef4p  12486  ef01bndlem  12548  sincosq4sgn  16056  binom4  16219  ppiublem2  16292  ppiqub  16293  chtqub  16296  bclbnd  16307  bposlem8  16318  lgsdir2lem3  16354