Definition df-4 11498

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 11490	. 2 class 4
2		c3 11489	. . 3 class 3
3		c1 10328	. . 3 class 1
4		caddc 10330	. . 3 class +
5	2, 3, 4	co 6970	. 2 class (3 + 1)
6	1, 5	wceq 1507	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  11517  4re  11518  4cn  11519  4pos  11547  4m1e3  11569  2p2e4  11575  3p1e4  11585  3p2e5  11591  4p4e8  11595  5p4e9  11598  3lt4  11614  halfpm6th  11661  6p4e10  11978  7p4e11  11982  7p7e14  11985  8p4e12  11988  8p6e14  11990  9p4e13  11995  9p5e14  11996  4t4e16  12005  5t4e20  12008  6t4e24  12012  7t4e28  12017  8t4e32  12023  9t4e36  12030  fz0to4untppr  12819  4bc2eq6  13497  bpoly3  15262  bpoly4  15263  fsumcube  15264  ef4p  15316  ef01bndlem  15387  ge2nprmge4  15891  lt6abl  18759  cphipval  23539  sincosq4sgn  24780  binom4  25119  quart1lem  25124  log2cnv  25214  ppiublem2  25471  ppiub  25472  chtub  25480  bclbnd  25548  bposlem8  25559  lgsdir2lem3  25595  3wlkdlem1  27678  ipval2  28251  problem3  32370  rmydioph  38952  rmxdioph  38954  expdiophlem2  38960  lt4addmuld  40948  stoweidlem13  41675  4even  43182  sbgoldbo  43260