Definition df-4 9043

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 9035	. 2 class 4
2		c3 9034	. . 3 class 3
3		c1 7873	. . 3 class 1
4		caddc 7875	. . 3 class +
5	2, 3, 4	co 5918	. 2 class (3 + 1)
6	1, 5	wceq 1364	1 wff 4 = (3 + 1)

This definition is referenced by:  4re  9059  4pos  9079  4m1e3  9103  2p2e4  9109  3p1e4  9117  3p2e5  9123  4p4e8  9127  5p4e9  9130  4nn  9145  3lt4  9154  halfpm6th  9202  6p4e10  9519  7p4e11  9523  7p7e14  9526  8p4e12  9529  8p6e14  9531  9p4e13  9536  9p5e14  9537  4t4e16  9546  5t4e20  9549  6t4e24  9553  7t4e28  9558  8t4e32  9564  9t4e36  9571  fz0to4untppr  10190  fzo0to42pr  10287  4bc2eq6  10845  ef4p  11837  ef01bndlem  11899  sincosq4sgn  14964  binom4  15111  lgsdir2lem3  15146