Definition df-4 9344

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 9336	. 2 class 4
2		c3 9335	. . 3 class 3
3		c1 8170	. . 3 class 1
4		caddc 8172	. . 3 class +
5	2, 3, 4	co 6075	. 2 class (3 + 1)
6	1, 5	wceq 1402	1 wff 4 = (3 + 1)

This definition is referenced by:  4re  9360  4pos  9380  4m1e3  9404  2p2e4  9410  3p1e4  9419  3p2e5  9425  4p4e8  9429  5p4e9  9432  4nn  9447  3lt4  9456  halfpm6th  9504  6p4e10  9827  7p4e11  9831  7p7e14  9834  8p4e12  9837  8p6e14  9839  9p4e13  9844  9p5e14  9845  4t4e16  9854  5t4e20  9857  6t4e24  9861  7t4e28  9866  8t4e32  9872  9t4e36  9879  fz0to4untppr  10509  fzo0to42pr  10616  4bc2eq6  11191  ef4p  12439  ef01bndlem  12501  sincosq4sgn  15853  binom4  16004  lgsdir2lem3  16063