Definition df-4 12241

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 12233	. 2 class 4
2		c3 12232	. . 3 class 3
3		c1 11035	. . 3 class 1
4		caddc 11037	. . 3 class +
5	2, 3, 4	co 7359	. 2 class (3 + 1)
6	1, 5	wceq 1548	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12259  4re  12260  4cn  12261  4pos  12283  4m1e3  12300  2p2e4  12306  3p1e4  12316  3p2e5  12322  4p4e8  12326  5p4e9  12329  3lt4  12345  6p4e10  12711  7p4e11  12715  7p7e14  12718  8p4e12  12721  8p6e14  12723  9p4e13  12728  9p5e14  12729  4t4e16  12738  5t4e20  12741  6t4e24  12745  7t4e28  12750  8t4e32  12756  9t4e36  12763  fz0to4untppr  13579  4bc2eq6  14286  bpoly3  16018  bpoly4  16019  fsumcube  16020  ef4p  16075  ef01bndlem  16146  ge2nprmge4  16666  lt6abl  19864  cphipval  25231  sincosq4sgn  26486  binom4  26835  quart1lem  26840  log2cnv  26929  ppiublem2  27187  ppiub  27188  chtub  27196  bclbnd  27264  bposlem8  27275  lgsdir2lem3  27311  3wlkdlem1  30249  ipval2  30798  problem3  35908  aks4d1p1p7  42572  rmydioph  43472  rmxdioph  43474  expdiophlem2  43480  lt4addmuld  45766  stoweidlem13  46468  sin5tlem2  47349  m1modnep2mod  47833  4even  48212  sbgoldbo  48290  ackval40  49196  ackval41a  49197  ackval42  49199