Definition df-4 11284

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 11275	. 2 class 4
2		c3 11274	. . 3 class 3
3		c1 10140	. . 3 class 1
4		caddc 10142	. . 3 class +
5	2, 3, 4	co 6794	. 2 class (3 + 1)
6	1, 5	wceq 1631	1 wff 4 = (3 + 1)

This definition is referenced by:  4re  11300  4pos  11319  4m1e3  11341  2p2e4  11347  3p1e4  11356  3p2e5  11363  4p4e8  11367  5p4e9  11370  6p4e10OLD  11374  4nn  11390  3lt4  11400  halfpm6th  11456  6p4e10  11800  7p4e11  11807  7p4e11OLD  11808  7p7e14  11811  8p4e12  11816  8p6e14  11818  9p4e13  11824  9p5e14  11825  4t4e16  11835  5t4e20  11839  5t4e20OLD  11840  6t4e24  11845  7t4e28  11852  8t4e32  11858  9t4e36  11867  fz0to4untppr  12651  fzo0to42pr  12764  4bc2eq6  13321  bpoly3  14996  bpoly4  14997  fsumcube  14998  ef4p  15050  ef01bndlem  15121  lt6abl  18504  cphipval  23262  iblitg  23756  sincosq4sgn  24475  ang180lem2  24762  binom4  24799  quart1lem  24804  log2cnv  24893  ppiublem2  25150  ppiub  25151  chtub  25159  bclbnd  25227  bposlem8  25238  lgsdir2lem3  25274  3wlkdlem1  27340  ipval2  27903  problem3  31900  rmydioph  38108  rmxdioph  38110  expdiophlem2  38116  lt4addmuld  40038  stoweidlem13  40748  4even  42147  sbgoldbo  42204