Definition df-4 12243

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 12235	. 2 class 4
2		c3 12234	. . 3 class 3
3		c1 11036	. . 3 class 1
4		caddc 11038	. . 3 class +
5	2, 3, 4	co 7364	. 2 class (3 + 1)
6	1, 5	wceq 1542	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12261  4re  12262  4cn  12263  4pos  12285  4m1e3  12302  2p2e4  12308  3p1e4  12318  3p2e5  12324  4p4e8  12328  5p4e9  12331  3lt4  12347  6p4e10  12713  7p4e11  12717  7p7e14  12720  8p4e12  12723  8p6e14  12725  9p4e13  12730  9p5e14  12731  4t4e16  12740  5t4e20  12743  6t4e24  12747  7t4e28  12752  8t4e32  12758  9t4e36  12765  fz0to4untppr  13581  4bc2eq6  14288  bpoly3  16020  bpoly4  16021  fsumcube  16022  ef4p  16077  ef01bndlem  16148  ge2nprmge4  16668  lt6abl  19867  cphipval  25207  sincosq4sgn  26462  binom4  26811  quart1lem  26816  log2cnv  26905  ppiublem2  27163  ppiub  27164  chtub  27172  bclbnd  27240  bposlem8  27251  lgsdir2lem3  27287  3wlkdlem1  30226  ipval2  30775  problem3  35846  aks4d1p1p7  42510  rmydioph  43439  rmxdioph  43441  expdiophlem2  43447  lt4addmuld  45736  stoweidlem13  46438  sin5tlem2  47317  m1modnep2mod  47797  4even  48176  sbgoldbo  48254  ackval40  49160  ackval41a  49161  ackval42  49163