Definition df-4 8774

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 8766	. 2 class 4
2		c3 8765	. . 3 class 3
3		c1 7614	. . 3 class 1
4		caddc 7616	. . 3 class +
5	2, 3, 4	co 5767	. 2 class ( 3 + 1 )
6	1, 5	wceq 1331	1 wff 4 = ( 3 + 1 )

This definition is referenced by:  4re  8790  4pos  8810  4m1e3  8834  2p2e4  8840  3p1e4  8848  3p2e5  8854  4p4e8  8858  5p4e9  8861  4nn  8876  3lt4  8885  halfpm6th  8933  6p4e10  9246  7p4e11  9250  7p7e14  9253  8p4e12  9256  8p6e14  9258  9p4e13  9263  9p5e14  9264  4t4e16  9273  5t4e20  9276  6t4e24  9280  7t4e28  9285  8t4e32  9291  9t4e36  9298  fzo0to42pr  9990  4bc2eq6  10513  ef4p  11389  ef01bndlem  11452  sincosq4sgn  12899