Definition df-4 9300

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 9292	. 2 class 4
2		c3 9291	. . 3 class 3
3		c1 8130	. . 3 class 1
4		caddc 8132	. . 3 class +
5	2, 3, 4	co 6052	. 2 class ( 3 + 1 )
6	1, 5	wceq 1398	1 wff 4 = ( 3 + 1 )

This definition is referenced by:  4re  9316  4pos  9336  4m1e3  9360  2p2e4  9366  3p1e4  9375  3p2e5  9381  4p4e8  9385  5p4e9  9388  4nn  9403  3lt4  9412  halfpm6th  9460  6p4e10  9783  7p4e11  9787  7p7e14  9790  8p4e12  9793  8p6e14  9795  9p4e13  9800  9p5e14  9801  4t4e16  9810  5t4e20  9813  6t4e24  9817  7t4e28  9822  8t4e32  9828  9t4e36  9835  fz0to4untppr  10462  fzo0to42pr  10569  4bc2eq6  11141  ef4p  12384  ef01bndlem  12446  sincosq4sgn  15711  binom4  15861  lgsdir2lem3  15920