Definition df-4 12376

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 12368	. 2 class 4
2		c3 12367	. . 3 class 3
3		c1 11172	. . 3 class 1
4		caddc 11174	. . 3 class +
5	2, 3, 4	co 7408	. 2 class (3 + 1)
6	1, 5	wceq 1570	1 wff 4 = (3 + 1)

This definition is used by:  4nn  12395  4re  12396  4cn  12397  4m1e3  12440  2p2e4  12446  3p1e4  12456  3p2e5  12462  4p4e8  12466  5p4e9  12469  3lt4  12488  6p4e10  12860  7p4e11  12864  7p7e14  12867  8p4e12  12870  8p6e14  12872  9p4e13  12877  9p5e14  12878  4t4e16  12887  5t4e20  12890  6t4e24  12894  7t4e28  12899  8t4e32  12905  9t4e36  12912  fz0to4untppr  13732  4bc2eq6  14440  bpoly3  16191  bpoly4  16192  fsumcube  16193  ef4p  16248  ef01bndlem  16319  ge2nprmge4  16839  lt6abl  20070  cphipval  25525  sincosq4sgn  26793  binom4  27141  quart1lem  27146  log2cnv  27235  ppiublem2  27493  ppiub  27494  chtub  27502  bclbnd  27570  bposlem8  27581  lgsdir2lem3  27617  3wlkdlem1  30693  ipval2  31242  problem3  36353  aks4d1p1p7  43044  1p4e5  43231  rmydioph  43959  rmxdioph  43961  expdiophlem2  43967  lt4addmuld  46243  stoweidlem13  46945  sin5tlem2  47842  goldpolyfactor  47849  m1modnep2mod  48350  4even  48729  sbgoldbo  48807  ackval40  49727  ackval41a  49728  ackval42  49730