Definition df-4 9070

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 9062	. 2 class 4
2		c3 9061	. . 3 class 3
3		c1 7899	. . 3 class 1
4		caddc 7901	. . 3 class +
5	2, 3, 4	co 5925	. 2 class (3 + 1)
6	1, 5	wceq 1364	1 wff 4 = (3 + 1)

This definition is referenced by:  4re  9086  4pos  9106  4m1e3  9130  2p2e4  9136  3p1e4  9145  3p2e5  9151  4p4e8  9155  5p4e9  9158  4nn  9173  3lt4  9182  halfpm6th  9230  6p4e10  9547  7p4e11  9551  7p7e14  9554  8p4e12  9557  8p6e14  9559  9p4e13  9564  9p5e14  9565  4t4e16  9574  5t4e20  9577  6t4e24  9581  7t4e28  9586  8t4e32  9592  9t4e36  9599  fz0to4untppr  10218  fzo0to42pr  10315  4bc2eq6  10885  ef4p  11878  ef01bndlem  11940  sincosq4sgn  15173  binom4  15323  lgsdir2lem3  15379