Definition df-4 12185

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 12177	. 2 class 4
2		c3 12176	. . 3 class 3
3		c1 11002	. . 3 class 1
4		caddc 11004	. . 3 class +
5	2, 3, 4	co 7341	. 2 class (3 + 1)
6	1, 5	wceq 1541	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12203  4re  12204  4cn  12205  4pos  12227  4m1e3  12244  2p2e4  12250  3p1e4  12260  3p2e5  12266  4p4e8  12270  5p4e9  12273  3lt4  12289  6p4e10  12655  7p4e11  12659  7p7e14  12662  8p4e12  12665  8p6e14  12667  9p4e13  12672  9p5e14  12673  4t4e16  12682  5t4e20  12685  6t4e24  12689  7t4e28  12694  8t4e32  12700  9t4e36  12707  fz0to4untppr  13525  4bc2eq6  14231  bpoly3  15960  bpoly4  15961  fsumcube  15962  ef4p  16017  ef01bndlem  16088  ge2nprmge4  16607  lt6abl  19802  cphipval  25165  sincosq4sgn  26432  binom4  26782  quart1lem  26787  log2cnv  26876  ppiublem2  27136  ppiub  27137  chtub  27145  bclbnd  27213  bposlem8  27224  lgsdir2lem3  27260  3wlkdlem1  30131  ipval2  30679  problem3  35703  aks4d1p1p7  42107  rmydioph  43047  rmxdioph  43049  expdiophlem2  43055  lt4addmuld  45347  stoweidlem13  46051  m1modnep2mod  47383  4even  47740  sbgoldbo  47818  ackval40  48725  ackval41a  48726  ackval42  48728