Definition df-4 9298

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 9290	. 2 class 4
2		c3 9289	. . 3 class 3
3		c1 8128	. . 3 class 1
4		caddc 8130	. . 3 class +
5	2, 3, 4	co 6050	. 2 class (3 + 1)
6	1, 5	wceq 1398	1 wff 4 = (3 + 1)

This definition is referenced by:  4re  9314  4pos  9334  4m1e3  9358  2p2e4  9364  3p1e4  9373  3p2e5  9379  4p4e8  9383  5p4e9  9386  4nn  9401  3lt4  9410  halfpm6th  9458  6p4e10  9780  7p4e11  9784  7p7e14  9787  8p4e12  9790  8p6e14  9792  9p4e13  9797  9p5e14  9798  4t4e16  9807  5t4e20  9810  6t4e24  9814  7t4e28  9819  8t4e32  9825  9t4e36  9832  fz0to4untppr  10458  fzo0to42pr  10565  4bc2eq6  11137  ef4p  12380  ef01bndlem  12442  sincosq4sgn  15694  binom4  15844  lgsdir2lem3  15903