Definition df-4 9347

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 9339	. 2 class 4
2		c3 9338	. . 3 class 3
3		c1 8173	. . 3 class 1
4		caddc 8175	. . 3 class +
5	2, 3, 4	co 6078	. 2 class ( 3 + 1 )
6	1, 5	wceq 1402	1 wff 4 = ( 3 + 1 )

This definition is referenced by:  4re  9363  4pos  9383  4m1e3  9407  2p2e4  9413  3p1e4  9422  3p2e5  9428  4p4e8  9432  5p4e9  9435  4nn  9450  3lt4  9459  halfpm6th  9507  6p4e10  9830  7p4e11  9834  7p7e14  9837  8p4e12  9840  8p6e14  9842  9p4e13  9847  9p5e14  9848  4t4e16  9857  5t4e20  9860  6t4e24  9864  7t4e28  9869  8t4e32  9875  9t4e36  9882  fz0to4untppr  10512  fzo0to42pr  10619  4bc2eq6  11194  ef4p  12442  ef01bndlem  12504  sincosq4sgn  15856  binom4  16007  lgsdir2lem3  16066