Definition df-4 12304

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 12296	. 2 class 4
2		c3 12295	. . 3 class 3
3		c1 11100	. . 3 class 1
4		caddc 11102	. . 3 class +
5	2, 3, 4	co 7410	. 2 class (3 + 1)
6	1, 5	wceq 1568	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12323  4re  12324  4cn  12325  4m1e3  12368  2p2e4  12374  3p1e4  12384  3p2e5  12390  4p4e8  12394  5p4e9  12397  3lt4  12416  6p4e10  12787  7p4e11  12791  7p7e14  12794  8p4e12  12797  8p6e14  12799  9p4e13  12804  9p5e14  12805  4t4e16  12814  5t4e20  12817  6t4e24  12821  7t4e28  12826  8t4e32  12832  9t4e36  12839  fz0to4untppr  13657  4bc2eq6  14364  bpoly3  16111  bpoly4  16112  fsumcube  16113  ef4p  16168  ef01bndlem  16239  ge2nprmge4  16759  lt6abl  19964  cphipval  25381  sincosq4sgn  26642  binom4  26991  quart1lem  26996  log2cnv  27085  ppiublem2  27343  ppiub  27344  chtub  27352  bclbnd  27420  bposlem8  27431  lgsdir2lem3  27467  3wlkdlem1  30476  ipval2  31025  problem3  36113  aks4d1p1p7  42787  rmydioph  43689  rmxdioph  43691  expdiophlem2  43697  lt4addmuld  45973  stoweidlem13  46675  sin5tlem2  47556  m1modnep2mod  48040  4even  48419  sbgoldbo  48497  ackval40  49418  ackval41a  49419  ackval42  49421