Definition df-4 8979

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 8971	. 2 class 4
2		c3 8970	. . 3 class 3
3		c1 7811	. . 3 class 1
4		caddc 7813	. . 3 class +
5	2, 3, 4	co 5874	. 2 class (3 + 1)
6	1, 5	wceq 1353	1 wff 4 = (3 + 1)

This definition is referenced by:  4re  8995  4pos  9015  4m1e3  9039  2p2e4  9045  3p1e4  9053  3p2e5  9059  4p4e8  9063  5p4e9  9066  4nn  9081  3lt4  9090  halfpm6th  9138  6p4e10  9454  7p4e11  9458  7p7e14  9461  8p4e12  9464  8p6e14  9466  9p4e13  9471  9p5e14  9472  4t4e16  9481  5t4e20  9484  6t4e24  9488  7t4e28  9493  8t4e32  9499  9t4e36  9506  fz0to4untppr  10123  fzo0to42pr  10219  4bc2eq6  10753  ef4p  11701  ef01bndlem  11763  sincosq4sgn  14220  binom4  14367  lgsdir2lem3  14401