Definition df-4 9315

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 9307	. 2 class 4
2		c3 9306	. . 3 class 3
3		c1 8144	. . 3 class 1
4		caddc 8146	. . 3 class +
5	2, 3, 4	co 6058	. 2 class (3 + 1)
6	1, 5	wceq 1398	1 wff 4 = (3 + 1)

This definition is referenced by:  4re  9331  4pos  9351  4m1e3  9375  2p2e4  9381  3p1e4  9390  3p2e5  9396  4p4e8  9400  5p4e9  9403  4nn  9418  3lt4  9427  halfpm6th  9475  6p4e10  9798  7p4e11  9802  7p7e14  9805  8p4e12  9808  8p6e14  9810  9p4e13  9815  9p5e14  9816  4t4e16  9825  5t4e20  9828  6t4e24  9832  7t4e28  9837  8t4e32  9843  9t4e36  9850  fz0to4untppr  10480  fzo0to42pr  10587  4bc2eq6  11162  ef4p  12405  ef01bndlem  12467  sincosq4sgn  15820  binom4  15970  lgsdir2lem3  16029