Definition df-4 12193

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 12185	. 2 class 4
2		c3 12184	. . 3 class 3
3		c1 11010	. . 3 class 1
4		caddc 11012	. . 3 class +
5	2, 3, 4	co 7349	. 2 class (3 + 1)
6	1, 5	wceq 1540	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12211  4re  12212  4cn  12213  4pos  12235  4m1e3  12252  2p2e4  12258  3p1e4  12268  3p2e5  12274  4p4e8  12278  5p4e9  12281  3lt4  12297  6p4e10  12663  7p4e11  12667  7p7e14  12670  8p4e12  12673  8p6e14  12675  9p4e13  12680  9p5e14  12681  4t4e16  12690  5t4e20  12693  6t4e24  12697  7t4e28  12702  8t4e32  12708  9t4e36  12715  fz0to4untppr  13533  4bc2eq6  14236  bpoly3  15965  bpoly4  15966  fsumcube  15967  ef4p  16022  ef01bndlem  16093  ge2nprmge4  16612  lt6abl  19774  cphipval  25141  sincosq4sgn  26408  binom4  26758  quart1lem  26763  log2cnv  26852  ppiublem2  27112  ppiub  27113  chtub  27121  bclbnd  27189  bposlem8  27200  lgsdir2lem3  27236  3wlkdlem1  30103  ipval2  30651  problem3  35640  aks4d1p1p7  42047  rmydioph  42987  rmxdioph  42989  expdiophlem2  42995  lt4addmuld  45288  stoweidlem13  45994  m1modnep2mod  47336  4even  47693  sbgoldbo  47771  ackval40  48678  ackval41a  48679  ackval42  48681