Definition df-4 9099

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 9091	. 2 class 4
2		c3 9090	. . 3 class 3
3		c1 7928	. . 3 class 1
4		caddc 7930	. . 3 class +
5	2, 3, 4	co 5946	. 2 class ( 3 + 1 )
6	1, 5	wceq 1373	1 wff 4 = ( 3 + 1 )

This definition is referenced by:  4re  9115  4pos  9135  4m1e3  9159  2p2e4  9165  3p1e4  9174  3p2e5  9180  4p4e8  9184  5p4e9  9187  4nn  9202  3lt4  9211  halfpm6th  9259  6p4e10  9577  7p4e11  9581  7p7e14  9584  8p4e12  9587  8p6e14  9589  9p4e13  9594  9p5e14  9595  4t4e16  9604  5t4e20  9607  6t4e24  9611  7t4e28  9616  8t4e32  9622  9t4e36  9629  fz0to4untppr  10248  fzo0to42pr  10351  4bc2eq6  10921  ef4p  12038  ef01bndlem  12100  sincosq4sgn  15334  binom4  15484  lgsdir2lem3  15540