Definition df-4 9263

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 9255	. 2 class 4
2		c3 9254	. . 3 class 3
3		c1 8093	. . 3 class 1
4		caddc 8095	. . 3 class +
5	2, 3, 4	co 6028	. 2 class (3 + 1)
6	1, 5	wceq 1398	1 wff 4 = (3 + 1)

This definition is referenced by:  4re  9279  4pos  9299  4m1e3  9323  2p2e4  9329  3p1e4  9338  3p2e5  9344  4p4e8  9348  5p4e9  9351  4nn  9366  3lt4  9375  halfpm6th  9423  6p4e10  9743  7p4e11  9747  7p7e14  9750  8p4e12  9753  8p6e14  9755  9p4e13  9760  9p5e14  9761  4t4e16  9770  5t4e20  9773  6t4e24  9777  7t4e28  9782  8t4e32  9788  9t4e36  9795  fz0to4untppr  10421  fzo0to42pr  10528  4bc2eq6  11099  ef4p  12335  ef01bndlem  12397  sincosq4sgn  15640  binom4  15790  lgsdir2lem3  15849