Definition df-4 12330

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 12322	. 2 class 4
2		c3 12321	. . 3 class 3
3		c1 11126	. . 3 class 1
4		caddc 11128	. . 3 class +
5	2, 3, 4	co 7416	. 2 class (3 + 1)
6	1, 5	wceq 1570	1 wff 4 = (3 + 1)

This definition is used by:  4nn  12349  4re  12350  4cn  12351  4m1e3  12394  2p2e4  12400  3p1e4  12410  3p2e5  12416  4p4e8  12420  5p4e9  12423  3lt4  12442  6p4e10  12814  7p4e11  12818  7p7e14  12821  8p4e12  12824  8p6e14  12826  9p4e13  12831  9p5e14  12832  4t4e16  12841  5t4e20  12844  6t4e24  12848  7t4e28  12853  8t4e32  12859  9t4e36  12866  fz0to4untppr  13685  4bc2eq6  14393  bpoly3  16146  bpoly4  16147  fsumcube  16148  ef4p  16203  ef01bndlem  16274  ge2nprmge4  16794  lt6abl  20021  cphipval  25470  sincosq4sgn  26734  binom4  27083  quart1lem  27088  log2cnv  27177  ppiublem2  27435  ppiub  27436  chtub  27444  bclbnd  27512  bposlem8  27523  lgsdir2lem3  27559  3wlkdlem1  30623  ipval2  31172  problem3  36231  aks4d1p1p7  42925  1p4e5  43112  rmydioph  43840  rmxdioph  43842  expdiophlem2  43848  lt4addmuld  46124  stoweidlem13  46826  sin5tlem2  47723  goldpolyfactor  47730  m1modnep2mod  48231  4even  48610  sbgoldbo  48688  ackval40  49608  ackval41a  49609  ackval42  49611