Definition df-4 9207

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 9199	. 2 class 4
2		c3 9198	. . 3 class 3
3		c1 8036	. . 3 class 1
4		caddc 8038	. . 3 class +
5	2, 3, 4	co 6021	. 2 class ( 3 + 1 )
6	1, 5	wceq 1397	1 wff 4 = ( 3 + 1 )

This definition is referenced by:  4re  9223  4pos  9243  4m1e3  9267  2p2e4  9273  3p1e4  9282  3p2e5  9288  4p4e8  9292  5p4e9  9295  4nn  9310  3lt4  9319  halfpm6th  9367  6p4e10  9685  7p4e11  9689  7p7e14  9692  8p4e12  9695  8p6e14  9697  9p4e13  9702  9p5e14  9703  4t4e16  9712  5t4e20  9715  6t4e24  9719  7t4e28  9724  8t4e32  9730  9t4e36  9737  fz0to4untppr  10362  fzo0to42pr  10469  4bc2eq6  11040  ef4p  12276  ef01bndlem  12338  sincosq4sgn  15580  binom4  15730  lgsdir2lem3  15786