Definition df-4 9367

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 9359	. 2 class 4
2		c3 9358	. . 3 class 3
3		c1 8180	. . 3 class 1
4		caddc 8182	. . 3 class +
5	2, 3, 4	co 6085	. 2 class ( 3 + 1 )
6	1, 5	wceq 1402	1 wff 4 = ( 3 + 1 )

This definition is used by:  4re  9383  4pos  9403  4m1e3  9427  2p2e4  9433  3p1e4  9442  3p2e5  9448  4p4e8  9452  5p4e9  9455  4nn  9472  3lt4  9481  halfpm6th  9529  6p4e10  9857  7p4e11  9861  7p7e14  9864  8p4e12  9867  8p6e14  9869  9p4e13  9874  9p5e14  9875  4t4e16  9884  5t4e20  9887  6t4e24  9891  7t4e28  9896  8t4e32  9902  9t4e36  9909  fz0to4untppr  10541  fzo0to42pr  10648  4bc2eq6  11227  ef4p  12477  ef01bndlem  12539  sincosq4sgn  15980  binom4  16138  ppiublem2  16193  ppiqub  16194  bclbnd  16205  lgsdir2lem3  16247