Definition df-4 8909

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 8901	. 2 class 4
2		c3 8900	. . 3 class 3
3		c1 7745	. . 3 class 1
4		caddc 7747	. . 3 class +
5	2, 3, 4	co 5836	. 2 class (3 + 1)
6	1, 5	wceq 1342	1 wff 4 = (3 + 1)

This definition is referenced by:  4re  8925  4pos  8945  4m1e3  8969  2p2e4  8975  3p1e4  8983  3p2e5  8989  4p4e8  8993  5p4e9  8996  4nn  9011  3lt4  9020  halfpm6th  9068  6p4e10  9384  7p4e11  9388  7p7e14  9391  8p4e12  9394  8p6e14  9396  9p4e13  9401  9p5e14  9402  4t4e16  9411  5t4e20  9414  6t4e24  9418  7t4e28  9423  8t4e32  9429  9t4e36  9436  fz0to4untppr  10049  fzo0to42pr  10145  4bc2eq6  10676  ef4p  11621  ef01bndlem  11683  sincosq4sgn  13291  binom4  13438