Definition df-4 12181

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 12173	. 2 class 4
2		c3 12172	. . 3 class 3
3		c1 10998	. . 3 class 1
4		caddc 11000	. . 3 class +
5	2, 3, 4	co 7340	. 2 class (3 + 1)
6	1, 5	wceq 1540	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12199  4re  12200  4cn  12201  4pos  12223  4m1e3  12240  2p2e4  12246  3p1e4  12256  3p2e5  12262  4p4e8  12266  5p4e9  12269  3lt4  12285  6p4e10  12651  7p4e11  12655  7p7e14  12658  8p4e12  12661  8p6e14  12663  9p4e13  12668  9p5e14  12669  4t4e16  12678  5t4e20  12681  6t4e24  12685  7t4e28  12690  8t4e32  12696  9t4e36  12703  fz0to4untppr  13521  4bc2eq6  14224  bpoly3  15952  bpoly4  15953  fsumcube  15954  ef4p  16009  ef01bndlem  16080  ge2nprmge4  16599  lt6abl  19761  cphipval  25124  sincosq4sgn  26391  binom4  26741  quart1lem  26746  log2cnv  26835  ppiublem2  27095  ppiub  27096  chtub  27104  bclbnd  27172  bposlem8  27183  lgsdir2lem3  27219  3wlkdlem1  30090  ipval2  30638  problem3  35657  aks4d1p1p7  42064  rmydioph  43004  rmxdioph  43006  expdiophlem2  43012  lt4addmuld  45304  stoweidlem13  46008  m1modnep2mod  47350  4even  47707  sbgoldbo  47785  ackval40  48692  ackval41a  48693  ackval42  48695