Definition df-4 12284

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 12276	. 2 class 4
2		c3 12275	. . 3 class 3
3		c1 11076	. . 3 class 1
4		caddc 11078	. . 3 class +
5	2, 3, 4	co 7398	. 2 class (3 + 1)
6	1, 5	wceq 1562	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12303  4re  12304  4cn  12305  4m1e3  12348  2p2e4  12354  3p1e4  12364  3p2e5  12370  4p4e8  12374  5p4e9  12377  3lt4  12396  6p4e10  12767  7p4e11  12771  7p7e14  12774  8p4e12  12777  8p6e14  12779  9p4e13  12784  9p5e14  12785  4t4e16  12794  5t4e20  12797  6t4e24  12801  7t4e28  12806  8t4e32  12812  9t4e36  12819  fz0to4untppr  13637  4bc2eq6  14344  bpoly3  16090  bpoly4  16091  fsumcube  16092  ef4p  16147  ef01bndlem  16218  ge2nprmge4  16738  lt6abl  19937  cphipval  25307  sincosq4sgn  26568  binom4  26917  quart1lem  26922  log2cnv  27011  ppiublem2  27269  ppiub  27270  chtub  27278  bclbnd  27346  bposlem8  27357  lgsdir2lem3  27393  3wlkdlem1  30363  ipval2  30912  problem3  36022  aks4d1p1p7  42696  rmydioph  43596  rmxdioph  43598  expdiophlem2  43604  lt4addmuld  45890  stoweidlem13  46592  sin5tlem2  47473  m1modnep2mod  47957  4even  48336  sbgoldbo  48414  ackval40  49320  ackval41a  49321  ackval42  49323