Definition df-4 12328

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 12320	. 2 class 4
2		c3 12319	. . 3 class 3
3		c1 11153	. . 3 class 1
4		caddc 11155	. . 3 class +
5	2, 3, 4	co 7430	. 2 class (3 + 1)
6	1, 5	wceq 1536	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12346  4re  12347  4cn  12348  4pos  12370  4m1e3  12392  2p2e4  12398  3p1e4  12408  3p2e5  12414  4p4e8  12418  5p4e9  12421  3lt4  12437  halfpm6th  12484  6p4e10  12802  7p4e11  12806  7p7e14  12809  8p4e12  12812  8p6e14  12814  9p4e13  12819  9p5e14  12820  4t4e16  12829  5t4e20  12832  6t4e24  12836  7t4e28  12841  8t4e32  12847  9t4e36  12854  fz0to4untppr  13666  4bc2eq6  14364  bpoly3  16090  bpoly4  16091  fsumcube  16092  ef4p  16145  ef01bndlem  16216  ge2nprmge4  16734  lt6abl  19927  cphipval  25290  sincosq4sgn  26557  binom4  26907  quart1lem  26912  log2cnv  27001  ppiublem2  27261  ppiub  27262  chtub  27270  bclbnd  27338  bposlem8  27349  lgsdir2lem3  27385  3wlkdlem1  30187  ipval2  30735  problem3  35651  aks4d1p1p7  42055  rmydioph  43002  rmxdioph  43004  expdiophlem2  43010  lt4addmuld  45256  stoweidlem13  45968  m1modnep2mod  47291  4even  47633  sbgoldbo  47711  ackval40  48542  ackval41a  48543  ackval42  48545