Definition df-4 9204

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 9196	. 2 class 4
2		c3 9195	. . 3 class 3
3		c1 8033	. . 3 class 1
4		caddc 8035	. . 3 class +
5	2, 3, 4	co 6018	. 2 class ( 3 + 1 )
6	1, 5	wceq 1397	1 wff 4 = ( 3 + 1 )

This definition is referenced by:  4re  9220  4pos  9240  4m1e3  9264  2p2e4  9270  3p1e4  9279  3p2e5  9285  4p4e8  9289  5p4e9  9292  4nn  9307  3lt4  9316  halfpm6th  9364  6p4e10  9682  7p4e11  9686  7p7e14  9689  8p4e12  9692  8p6e14  9694  9p4e13  9699  9p5e14  9700  4t4e16  9709  5t4e20  9712  6t4e24  9716  7t4e28  9721  8t4e32  9727  9t4e36  9734  fz0to4untppr  10359  fzo0to42pr  10465  4bc2eq6  11036  ef4p  12256  ef01bndlem  12318  sincosq4sgn  15555  binom4  15705  lgsdir2lem3  15761