Definition df-4 9010

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 9002	. 2 class 4
2		c3 9001	. . 3 class 3
3		c1 7842	. . 3 class 1
4		caddc 7844	. . 3 class +
5	2, 3, 4	co 5896	. 2 class ( 3 + 1 )
6	1, 5	wceq 1364	1 wff 4 = ( 3 + 1 )

This definition is referenced by:  4re  9026  4pos  9046  4m1e3  9070  2p2e4  9076  3p1e4  9084  3p2e5  9090  4p4e8  9094  5p4e9  9097  4nn  9112  3lt4  9121  halfpm6th  9169  6p4e10  9485  7p4e11  9489  7p7e14  9492  8p4e12  9495  8p6e14  9497  9p4e13  9502  9p5e14  9503  4t4e16  9512  5t4e20  9515  6t4e24  9519  7t4e28  9524  8t4e32  9530  9t4e36  9537  fz0to4untppr  10154  fzo0to42pr  10250  4bc2eq6  10786  ef4p  11734  ef01bndlem  11796  sincosq4sgn  14710  binom4  14857  lgsdir2lem3  14892