Definition df-4 9368

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 9360	. 2 class 4
2		c3 9359	. . 3 class 3
3		c1 8181	. . 3 class 1
4		caddc 8183	. . 3 class +
5	2, 3, 4	co 6085	. 2 class (3 + 1)
6	1, 5	wceq 1402	1 wff 4 = (3 + 1)

This definition is used by:  4re  9384  4pos  9404  4m1e3  9428  2p2e4  9434  3p1e4  9443  3p2e5  9449  4p4e8  9453  5p4e9  9456  4nn  9473  3lt4  9482  halfpm6th  9530  6p4e10  9858  7p4e11  9862  7p7e14  9865  8p4e12  9868  8p6e14  9870  9p4e13  9875  9p5e14  9876  4t4e16  9885  5t4e20  9888  6t4e24  9892  7t4e28  9897  8t4e32  9903  9t4e36  9910  fz0to4untppr  10542  fzo0to42pr  10649  4bc2eq6  11228  ef4p  12479  ef01bndlem  12541  sincosq4sgn  15983  binom4  16141  ppiublem2  16214  ppiqub  16215  chtqub  16218  bclbnd  16229  lgsdir2lem3  16271