Definition df-4 9117

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 9109	. 2 class 4
2		c3 9108	. . 3 class 3
3		c1 7946	. . 3 class 1
4		caddc 7948	. . 3 class +
5	2, 3, 4	co 5957	. 2 class (3 + 1)
6	1, 5	wceq 1373	1 wff 4 = (3 + 1)

This definition is referenced by:  4re  9133  4pos  9153  4m1e3  9177  2p2e4  9183  3p1e4  9192  3p2e5  9198  4p4e8  9202  5p4e9  9205  4nn  9220  3lt4  9229  halfpm6th  9277  6p4e10  9595  7p4e11  9599  7p7e14  9602  8p4e12  9605  8p6e14  9607  9p4e13  9612  9p5e14  9613  4t4e16  9622  5t4e20  9625  6t4e24  9629  7t4e28  9634  8t4e32  9640  9t4e36  9647  fz0to4untppr  10266  fzo0to42pr  10371  4bc2eq6  10941  ef4p  12080  ef01bndlem  12142  sincosq4sgn  15376  binom4  15526  lgsdir2lem3  15582