Definition df-4 11081

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 11072	. 2 class 4
2		c3 11071	. . 3 class 3
3		c1 9937	. . 3 class 1
4		caddc 9939	. . 3 class +
5	2, 3, 4	co 6650	. 2 class (3 + 1)
6	1, 5	wceq 1483	1 wff 4 = (3 + 1)

This definition is referenced by:  4re  11097  4pos  11116  4m1e3  11138  2p2e4  11144  3p1e4  11153  3p2e5  11160  4p4e8  11164  5p4e9  11167  6p4e10OLD  11171  4nn  11187  3lt4  11197  halfpm6th  11253  6p4e10  11598  7p4e11  11605  7p4e11OLD  11606  7p7e14  11609  8p4e12  11614  8p6e14  11616  9p4e13  11622  9p5e14  11623  4t4e16  11633  5t4e20  11637  5t4e20OLD  11638  6t4e24  11643  7t4e28  11650  8t4e32  11656  9t4e36  11665  fz0to4untppr  12442  fzo0to42pr  12555  4bc2eq6  13116  bpoly3  14789  bpoly4  14790  fsumcube  14791  ef4p  14843  ef01bndlem  14914  lt6abl  18296  cphipval  23042  iblitg  23535  sincosq4sgn  24253  ang180lem2  24540  binom4  24577  quart1lem  24582  log2cnv  24671  ppiublem2  24928  ppiub  24929  chtub  24937  bclbnd  25005  bposlem8  25016  lgsdir2lem3  25052  3wlkdlem1  27019  ipval2  27562  problem3  31561  rmydioph  37581  rmxdioph  37583  expdiophlem2  37589  lt4addmuld  39520  stoweidlem13  40230  4even  41618  sbgoldbo  41675