Definition df-4 8639

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 8631	. 2 class 4
2		c3 8630	. . 3 class 3
3		c1 7501	. . 3 class 1
4		caddc 7503	. . 3 class +
5	2, 3, 4	co 5706	. 2 class ( 3 + 1 )
6	1, 5	wceq 1299	1 wff 4 = ( 3 + 1 )

This definition is referenced by:  4re  8655  4pos  8675  2p2e4  8699  3p1e4  8707  3p2e5  8713  4p4e8  8717  5p4e9  8720  4nn  8735  3lt4  8744  halfpm6th  8792  6p4e10  9105  7p4e11  9109  7p7e14  9112  8p4e12  9115  8p6e14  9117  9p4e13  9122  9p5e14  9123  4t4e16  9132  5t4e20  9135  6t4e24  9139  7t4e28  9144  8t4e32  9150  9t4e36  9157  fzo0to42pr  9838  4bc2eq6  10361  ef4p  11198  ef01bndlem  11261