Definition df-4 12208

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 12200	. 2 class 4
2		c3 12199	. . 3 class 3
3		c1 11025	. . 3 class 1
4		caddc 11027	. . 3 class +
5	2, 3, 4	co 7356	. 2 class (3 + 1)
6	1, 5	wceq 1541	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12226  4re  12227  4cn  12228  4pos  12250  4m1e3  12267  2p2e4  12273  3p1e4  12283  3p2e5  12289  4p4e8  12293  5p4e9  12296  3lt4  12312  6p4e10  12677  7p4e11  12681  7p7e14  12684  8p4e12  12687  8p6e14  12689  9p4e13  12694  9p5e14  12695  4t4e16  12704  5t4e20  12707  6t4e24  12711  7t4e28  12716  8t4e32  12722  9t4e36  12729  fz0to4untppr  13544  4bc2eq6  14250  bpoly3  15979  bpoly4  15980  fsumcube  15981  ef4p  16036  ef01bndlem  16107  ge2nprmge4  16626  lt6abl  19822  cphipval  25197  sincosq4sgn  26464  binom4  26814  quart1lem  26819  log2cnv  26908  ppiublem2  27168  ppiub  27169  chtub  27177  bclbnd  27245  bposlem8  27256  lgsdir2lem3  27292  3wlkdlem1  30183  ipval2  30731  problem3  35810  aks4d1p1p7  42267  rmydioph  43198  rmxdioph  43200  expdiophlem2  43206  lt4addmuld  45496  stoweidlem13  46199  m1modnep2mod  47540  4even  47897  sbgoldbo  47975  ackval40  48881  ackval41a  48882  ackval42  48884