Definition df-4 12358

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 12350	. 2 class 4
2		c3 12349	. . 3 class 3
3		c1 11185	. . 3 class 1
4		caddc 11187	. . 3 class +
5	2, 3, 4	co 7448	. 2 class (3 + 1)
6	1, 5	wceq 1537	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12376  4re  12377  4cn  12378  4pos  12400  4m1e3  12422  2p2e4  12428  3p1e4  12438  3p2e5  12444  4p4e8  12448  5p4e9  12451  3lt4  12467  halfpm6th  12514  6p4e10  12830  7p4e11  12834  7p7e14  12837  8p4e12  12840  8p6e14  12842  9p4e13  12847  9p5e14  12848  4t4e16  12857  5t4e20  12860  6t4e24  12864  7t4e28  12869  8t4e32  12875  9t4e36  12882  fz0to4untppr  13687  4bc2eq6  14378  bpoly3  16106  bpoly4  16107  fsumcube  16108  ef4p  16161  ef01bndlem  16232  ge2nprmge4  16748  lt6abl  19937  cphipval  25296  sincosq4sgn  26561  binom4  26911  quart1lem  26916  log2cnv  27005  ppiublem2  27265  ppiub  27266  chtub  27274  bclbnd  27342  bposlem8  27353  lgsdir2lem3  27389  3wlkdlem1  30191  ipval2  30739  problem3  35635  aks4d1p1p7  42031  rmydioph  42971  rmxdioph  42973  expdiophlem2  42979  lt4addmuld  45221  stoweidlem13  45934  4even  47583  sbgoldbo  47661  ackval40  48427  ackval41a  48428  ackval42  48430