Definition df-4 12331

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 12323	. 2 class 4
2		c3 12322	. . 3 class 3
3		c1 11156	. . 3 class 1
4		caddc 11158	. . 3 class +
5	2, 3, 4	co 7431	. 2 class (3 + 1)
6	1, 5	wceq 1540	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12349  4re  12350  4cn  12351  4pos  12373  4m1e3  12395  2p2e4  12401  3p1e4  12411  3p2e5  12417  4p4e8  12421  5p4e9  12424  3lt4  12440  halfpm6th  12487  6p4e10  12805  7p4e11  12809  7p7e14  12812  8p4e12  12815  8p6e14  12817  9p4e13  12822  9p5e14  12823  4t4e16  12832  5t4e20  12835  6t4e24  12839  7t4e28  12844  8t4e32  12850  9t4e36  12857  fz0to4untppr  13670  4bc2eq6  14368  bpoly3  16094  bpoly4  16095  fsumcube  16096  ef4p  16149  ef01bndlem  16220  ge2nprmge4  16738  lt6abl  19913  cphipval  25277  sincosq4sgn  26543  binom4  26893  quart1lem  26898  log2cnv  26987  ppiublem2  27247  ppiub  27248  chtub  27256  bclbnd  27324  bposlem8  27335  lgsdir2lem3  27371  3wlkdlem1  30178  ipval2  30726  problem3  35672  aks4d1p1p7  42075  rmydioph  43026  rmxdioph  43028  expdiophlem2  43034  lt4addmuld  45318  stoweidlem13  46028  m1modnep2mod  47354  4even  47696  sbgoldbo  47774  ackval40  48614  ackval41a  48615  ackval42  48617