Definition df-4 12407

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 12399	. 2 class 4
2		c3 12398	. . 3 class 3
3		c1 11201	. . 3 class 1
4		caddc 11203	. . 3 class +
5	2, 3, 4	co 7420	. 2 class (3 + 1)
6	1, 5	wceq 1569	1 wff 4 = (3 + 1)

This definition is used by:  4nn  12426  4re  12427  4cn  12428  4m1e3  12471  2p2e4  12477  3p1e4  12487  3p2e5  12493  4p4e8  12497  5p4e9  12500  3lt4  12519  6p4e10  12891  7p4e11  12895  7p7e14  12898  8p4e12  12901  8p6e14  12903  9p4e13  12908  9p5e14  12909  4t4e16  12918  5t4e20  12921  6t4e24  12925  7t4e28  12930  8t4e32  12936  9t4e36  12943  fz0to4untppr  13764  4bc2eq6  14473  bpoly3  16224  bpoly4  16225  fsumcube  16226  ef4p  16281  ef01bndlem  16352  ge2nprmge4  16877  lt6abl  20109  cphipval  25564  sincosq4sgn  26830  binom4  27178  quart1lem  27183  log2cnv  27272  ppiublem2  27530  ppiub  27531  chtub  27539  bclbnd  27607  bposlem8  27618  lgsdir2lem3  27654  3wlkdlem1  30760  ipval2  31309  problem3  36474  aks4d1p1p7  43167  1p4e5  43354  rmydioph  44063  rmxdioph  44065  expdiophlem2  44071  lt4addmuld  46364  stoweidlem13  47065  sin5tlem2  47962  goldpolyfactor  47969  m1modnep2mod  48470  4even  48849  sbgoldbo  48927  ackval40  49847  ackval41a  49848  ackval42  49850