Definition df-4 9096

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 9088	. 2 class 4
2		c3 9087	. . 3 class 3
3		c1 7925	. . 3 class 1
4		caddc 7927	. . 3 class +
5	2, 3, 4	co 5943	. 2 class (3 + 1)
6	1, 5	wceq 1372	1 wff 4 = (3 + 1)

This definition is referenced by:  4re  9112  4pos  9132  4m1e3  9156  2p2e4  9162  3p1e4  9171  3p2e5  9177  4p4e8  9181  5p4e9  9184  4nn  9199  3lt4  9208  halfpm6th  9256  6p4e10  9574  7p4e11  9578  7p7e14  9581  8p4e12  9584  8p6e14  9586  9p4e13  9591  9p5e14  9592  4t4e16  9601  5t4e20  9604  6t4e24  9608  7t4e28  9613  8t4e32  9619  9t4e36  9626  fz0to4untppr  10245  fzo0to42pr  10347  4bc2eq6  10917  ef4p  11947  ef01bndlem  12009  sincosq4sgn  15243  binom4  15393  lgsdir2lem3  15449