Definition df-4 12431

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 12423	. 2 class 4
2		c3 12422	. . 3 class 3
3		c1 11225	. . 3 class 1
4		caddc 11227	. . 3 class +
5	2, 3, 4	co 7440	. 2 class (3 + 1)
6	1, 5	wceq 1570	1 wff 4 = (3 + 1)

This definition is used by:  4nn  12450  4re  12451  4cn  12452  4m1e3  12495  2p2e4  12501  3p1e4  12511  3p2e5  12517  4p4e8  12521  5p4e9  12524  3lt4  12543  6p4e10  12915  7p4e11  12919  7p7e14  12922  8p4e12  12925  8p6e14  12927  9p4e13  12932  9p5e14  12933  4t4e16  12942  5t4e20  12945  6t4e24  12949  7t4e28  12954  8t4e32  12960  9t4e36  12967  fz0to4untppr  13788  4bc2eq6  14497  bpoly3  16250  bpoly4  16251  fsumcube  16252  ef4p  16307  ef01bndlem  16378  ge2nprmge4  16903  lt6abl  20136  cphipval  25591  sincosq4sgn  26857  binom4  27205  quart1lem  27210  log2cnv  27299  ppiublem2  27557  ppiub  27558  chtub  27566  bclbnd  27634  bposlem8  27645  lgsdir2lem3  27681  3wlkdlem1  30787  ipval2  31336  problem3  36598  aks4d1p1p7  43315  1p4e5  43502  rmydioph  44212  rmxdioph  44214  expdiophlem2  44220  lt4addmuld  46525  stoweidlem13  47226  sin5tlem2  48123  goldpolyfactor  48130  m1modnep2mod  48631  4even  49010  sbgoldbo  49088  ackval40  50008  ackval41a  50009  ackval42  50011