Definition df-4 11703

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 11695	. 2 class 4
2		c3 11694	. . 3 class 3
3		c1 10538	. . 3 class 1
4		caddc 10540	. . 3 class +
5	2, 3, 4	co 7156	. 2 class (3 + 1)
6	1, 5	wceq 1537	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  11721  4re  11722  4cn  11723  4pos  11745  4m1e3  11767  2p2e4  11773  3p1e4  11783  3p2e5  11789  4p4e8  11793  5p4e9  11796  3lt4  11812  halfpm6th  11859  6p4e10  12171  7p4e11  12175  7p7e14  12178  8p4e12  12181  8p6e14  12183  9p4e13  12188  9p5e14  12189  4t4e16  12198  5t4e20  12201  6t4e24  12205  7t4e28  12210  8t4e32  12216  9t4e36  12223  fz0to4untppr  13011  4bc2eq6  13690  bpoly3  15412  bpoly4  15413  fsumcube  15414  ef4p  15466  ef01bndlem  15537  ge2nprmge4  16045  lt6abl  19015  cphipval  23846  sincosq4sgn  25087  binom4  25428  quart1lem  25433  log2cnv  25522  ppiublem2  25779  ppiub  25780  chtub  25788  bclbnd  25856  bposlem8  25867  lgsdir2lem3  25903  3wlkdlem1  27938  ipval2  28484  problem3  32910  rmydioph  39660  rmxdioph  39662  expdiophlem2  39668  lt4addmuld  41622  stoweidlem13  42347  4even  43923  sbgoldbo  44001