Definition df-4 8918

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 8910	. 2 class 4
2		c3 8909	. . 3 class 3
3		c1 7754	. . 3 class 1
4		caddc 7756	. . 3 class +
5	2, 3, 4	co 5842	. 2 class (3 + 1)
6	1, 5	wceq 1343	1 wff 4 = (3 + 1)

This definition is referenced by:  4re  8934  4pos  8954  4m1e3  8978  2p2e4  8984  3p1e4  8992  3p2e5  8998  4p4e8  9002  5p4e9  9005  4nn  9020  3lt4  9029  halfpm6th  9077  6p4e10  9393  7p4e11  9397  7p7e14  9400  8p4e12  9403  8p6e14  9405  9p4e13  9410  9p5e14  9411  4t4e16  9420  5t4e20  9423  6t4e24  9427  7t4e28  9432  8t4e32  9438  9t4e36  9445  fz0to4untppr  10059  fzo0to42pr  10155  4bc2eq6  10687  ef4p  11635  ef01bndlem  11697  sincosq4sgn  13390  binom4  13537  lgsdir2lem3  13571