Definition df-4 9167

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 9159	. 2 class 4
2		c3 9158	. . 3 class 3
3		c1 7996	. . 3 class 1
4		caddc 7998	. . 3 class +
5	2, 3, 4	co 6000	. 2 class (3 + 1)
6	1, 5	wceq 1395	1 wff 4 = (3 + 1)

This definition is referenced by:  4re  9183  4pos  9203  4m1e3  9227  2p2e4  9233  3p1e4  9242  3p2e5  9248  4p4e8  9252  5p4e9  9255  4nn  9270  3lt4  9279  halfpm6th  9327  6p4e10  9645  7p4e11  9649  7p7e14  9652  8p4e12  9655  8p6e14  9657  9p4e13  9662  9p5e14  9663  4t4e16  9672  5t4e20  9675  6t4e24  9679  7t4e28  9684  8t4e32  9690  9t4e36  9697  fz0to4untppr  10316  fzo0to42pr  10421  4bc2eq6  10991  ef4p  12200  ef01bndlem  12262  sincosq4sgn  15497  binom4  15647  lgsdir2lem3  15703