Definition df-4 11860

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 11852	. 2 class 4
2		c3 11851	. . 3 class 3
3		c1 10695	. . 3 class 1
4		caddc 10697	. . 3 class +
5	2, 3, 4	co 7191	. 2 class (3 + 1)
6	1, 5	wceq 1543	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  11878  4re  11879  4cn  11880  4pos  11902  4m1e3  11924  2p2e4  11930  3p1e4  11940  3p2e5  11946  4p4e8  11950  5p4e9  11953  3lt4  11969  halfpm6th  12016  6p4e10  12330  7p4e11  12334  7p7e14  12337  8p4e12  12340  8p6e14  12342  9p4e13  12347  9p5e14  12348  4t4e16  12357  5t4e20  12360  6t4e24  12364  7t4e28  12369  8t4e32  12375  9t4e36  12382  fz0to4untppr  13180  4bc2eq6  13860  bpoly3  15583  bpoly4  15584  fsumcube  15585  ef4p  15637  ef01bndlem  15708  ge2nprmge4  16221  lt6abl  19234  cphipval  24094  sincosq4sgn  25345  binom4  25687  quart1lem  25692  log2cnv  25781  ppiublem2  26038  ppiub  26039  chtub  26047  bclbnd  26115  bposlem8  26126  lgsdir2lem3  26162  3wlkdlem1  28196  ipval2  28742  problem3  33292  aks4d1p1p7  39764  rmydioph  40480  rmxdioph  40482  expdiophlem2  40488  lt4addmuld  42459  stoweidlem13  43172  4even  44777  sbgoldbo  44855  ackval40  45655  ackval41a  45656  ackval42  45658