Definition df-4 9182

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 9174	. 2 class 4
2		c3 9173	. . 3 class 3
3		c1 8011	. . 3 class 1
4		caddc 8013	. . 3 class +
5	2, 3, 4	co 6007	. 2 class (3 + 1)
6	1, 5	wceq 1395	1 wff 4 = (3 + 1)

This definition is referenced by:  4re  9198  4pos  9218  4m1e3  9242  2p2e4  9248  3p1e4  9257  3p2e5  9263  4p4e8  9267  5p4e9  9270  4nn  9285  3lt4  9294  halfpm6th  9342  6p4e10  9660  7p4e11  9664  7p7e14  9667  8p4e12  9670  8p6e14  9672  9p4e13  9677  9p5e14  9678  4t4e16  9687  5t4e20  9690  6t4e24  9694  7t4e28  9699  8t4e32  9705  9t4e36  9712  fz0to4untppr  10332  fzo0to42pr  10438  4bc2eq6  11008  ef4p  12220  ef01bndlem  12282  sincosq4sgn  15518  binom4  15668  lgsdir2lem3  15724