Definition df-4 8100

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 8091	. 2 class 4
2		c3 8090	. . 3 class 3
3		c1 6982	. . 3 class 1
4		caddc 6984	. . 3 class +
5	2, 3, 4	co 5532	. 2 class (3 + 1)
6	1, 5	wceq 1284	1 wff 4 = (3 + 1)

This definition is referenced by:  4re  8116  4pos  8136  2p2e4  8159  3p1e4  8167  3p2e5  8173  4p4e8  8177  5p4e9  8180  4nn  8195  3lt4  8204  halfpm6th  8251  6p4e10  8548  7p4e11  8552  7p7e14  8555  8p4e12  8558  8p6e14  8560  9p4e13  8565  9p5e14  8566  4t4e16  8575  5t4e20  8578  6t4e24  8582  7t4e28  8587  8t4e32  8593  9t4e36  8600  fzo0to42pr  9229  4bc2eq6  9701