Definition df-4 9068

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 9060	. 2 class 4
2		c3 9059	. . 3 class 3
3		c1 7897	. . 3 class 1
4		caddc 7899	. . 3 class +
5	2, 3, 4	co 5925	. 2 class (3 + 1)
6	1, 5	wceq 1364	1 wff 4 = (3 + 1)

This definition is referenced by:  4re  9084  4pos  9104  4m1e3  9128  2p2e4  9134  3p1e4  9143  3p2e5  9149  4p4e8  9153  5p4e9  9156  4nn  9171  3lt4  9180  halfpm6th  9228  6p4e10  9545  7p4e11  9549  7p7e14  9552  8p4e12  9555  8p6e14  9557  9p4e13  9562  9p5e14  9563  4t4e16  9572  5t4e20  9575  6t4e24  9579  7t4e28  9584  8t4e32  9590  9t4e36  9597  fz0to4untppr  10216  fzo0to42pr  10313  4bc2eq6  10883  ef4p  11876  ef01bndlem  11938  sincosq4sgn  15149  binom4  15299  lgsdir2lem3  15355