Definition df-4 9097

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 9089	. 2 class 4
2		c3 9088	. . 3 class 3
3		c1 7926	. . 3 class 1
4		caddc 7928	. . 3 class +
5	2, 3, 4	co 5944	. 2 class ( 3 + 1 )
6	1, 5	wceq 1373	1 wff 4 = ( 3 + 1 )

This definition is referenced by:  4re  9113  4pos  9133  4m1e3  9157  2p2e4  9163  3p1e4  9172  3p2e5  9178  4p4e8  9182  5p4e9  9185  4nn  9200  3lt4  9209  halfpm6th  9257  6p4e10  9575  7p4e11  9579  7p7e14  9582  8p4e12  9585  8p6e14  9587  9p4e13  9592  9p5e14  9593  4t4e16  9602  5t4e20  9605  6t4e24  9609  7t4e28  9614  8t4e32  9620  9t4e36  9627  fz0to4untppr  10246  fzo0to42pr  10349  4bc2eq6  10919  ef4p  12005  ef01bndlem  12067  sincosq4sgn  15301  binom4  15451  lgsdir2lem3  15507