Definition df-4 9079

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 9071	. 2 class 4
2		c3 9070	. . 3 class 3
3		c1 7908	. . 3 class 1
4		caddc 7910	. . 3 class +
5	2, 3, 4	co 5934	. 2 class (3 + 1)
6	1, 5	wceq 1372	1 wff 4 = (3 + 1)

This definition is referenced by:  4re  9095  4pos  9115  4m1e3  9139  2p2e4  9145  3p1e4  9154  3p2e5  9160  4p4e8  9164  5p4e9  9167  4nn  9182  3lt4  9191  halfpm6th  9239  6p4e10  9557  7p4e11  9561  7p7e14  9564  8p4e12  9567  8p6e14  9569  9p4e13  9574  9p5e14  9575  4t4e16  9584  5t4e20  9587  6t4e24  9591  7t4e28  9596  8t4e32  9602  9t4e36  9609  fz0to4untppr  10228  fzo0to42pr  10330  4bc2eq6  10900  ef4p  11924  ef01bndlem  11986  sincosq4sgn  15219  binom4  15369  lgsdir2lem3  15425