Definition df-4 12214

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 12206	. 2 class 4
2		c3 12205	. . 3 class 3
3		c1 11031	. . 3 class 1
4		caddc 11033	. . 3 class +
5	2, 3, 4	co 7360	. 2 class (3 + 1)
6	1, 5	wceq 1542	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12232  4re  12233  4cn  12234  4pos  12256  4m1e3  12273  2p2e4  12279  3p1e4  12289  3p2e5  12295  4p4e8  12299  5p4e9  12302  3lt4  12318  6p4e10  12683  7p4e11  12687  7p7e14  12690  8p4e12  12693  8p6e14  12695  9p4e13  12700  9p5e14  12701  4t4e16  12710  5t4e20  12713  6t4e24  12717  7t4e28  12722  8t4e32  12728  9t4e36  12735  fz0to4untppr  13550  4bc2eq6  14256  bpoly3  15985  bpoly4  15986  fsumcube  15987  ef4p  16042  ef01bndlem  16113  ge2nprmge4  16632  lt6abl  19828  cphipval  25203  sincosq4sgn  26470  binom4  26820  quart1lem  26825  log2cnv  26914  ppiublem2  27174  ppiub  27175  chtub  27183  bclbnd  27251  bposlem8  27262  lgsdir2lem3  27298  3wlkdlem1  30238  ipval2  30786  problem3  35863  aks4d1p1p7  42396  rmydioph  43323  rmxdioph  43325  expdiophlem2  43331  lt4addmuld  45621  stoweidlem13  46324  m1modnep2mod  47665  4even  48022  sbgoldbo  48100  ackval40  49006  ackval41a  49007  ackval42  49009