Definition df-4 12279

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 12271	. 2 class 4
2		c3 12270	. . 3 class 3
3		c1 11113	. . 3 class 1
4		caddc 11115	. . 3 class +
5	2, 3, 4	co 7411	. 2 class (3 + 1)
6	1, 5	wceq 1541	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12297  4re  12298  4cn  12299  4pos  12321  4m1e3  12343  2p2e4  12349  3p1e4  12359  3p2e5  12365  4p4e8  12369  5p4e9  12372  3lt4  12388  halfpm6th  12435  6p4e10  12751  7p4e11  12755  7p7e14  12758  8p4e12  12761  8p6e14  12763  9p4e13  12768  9p5e14  12769  4t4e16  12778  5t4e20  12781  6t4e24  12785  7t4e28  12790  8t4e32  12796  9t4e36  12803  fz0to4untppr  13606  4bc2eq6  14291  bpoly3  16004  bpoly4  16005  fsumcube  16006  ef4p  16058  ef01bndlem  16129  ge2nprmge4  16640  lt6abl  19765  cphipval  24767  sincosq4sgn  26018  binom4  26362  quart1lem  26367  log2cnv  26456  ppiublem2  26713  ppiub  26714  chtub  26722  bclbnd  26790  bposlem8  26801  lgsdir2lem3  26837  3wlkdlem1  29450  ipval2  29998  problem3  34721  aks4d1p1p7  41031  rmydioph  41841  rmxdioph  41843  expdiophlem2  41849  lt4addmuld  44101  stoweidlem13  44814  4even  46462  sbgoldbo  46540  ackval40  47463  ackval41a  47464  ackval42  47466