Definition df-4 8781

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 8773	. 2 class 4
2		c3 8772	. . 3 class 3
3		c1 7621	. . 3 class 1
4		caddc 7623	. . 3 class +
5	2, 3, 4	co 5774	. 2 class ( 3 + 1 )
6	1, 5	wceq 1331	1 wff 4 = ( 3 + 1 )

This definition is referenced by:  4re  8797  4pos  8817  4m1e3  8841  2p2e4  8847  3p1e4  8855  3p2e5  8861  4p4e8  8865  5p4e9  8868  4nn  8883  3lt4  8892  halfpm6th  8940  6p4e10  9253  7p4e11  9257  7p7e14  9260  8p4e12  9263  8p6e14  9265  9p4e13  9270  9p5e14  9271  4t4e16  9280  5t4e20  9283  6t4e24  9287  7t4e28  9292  8t4e32  9298  9t4e36  9305  fzo0to42pr  9997  4bc2eq6  10520  ef4p  11400  ef01bndlem  11463  sincosq4sgn  12910