Definition df-4 12251

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 12243	. 2 class 4
2		c3 12242	. . 3 class 3
3		c1 11069	. . 3 class 1
4		caddc 11071	. . 3 class +
5	2, 3, 4	co 7387	. 2 class (3 + 1)
6	1, 5	wceq 1540	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12269  4re  12270  4cn  12271  4pos  12293  4m1e3  12310  2p2e4  12316  3p1e4  12326  3p2e5  12332  4p4e8  12336  5p4e9  12339  3lt4  12355  6p4e10  12721  7p4e11  12725  7p7e14  12728  8p4e12  12731  8p6e14  12733  9p4e13  12738  9p5e14  12739  4t4e16  12748  5t4e20  12751  6t4e24  12755  7t4e28  12760  8t4e32  12766  9t4e36  12773  fz0to4untppr  13591  4bc2eq6  14294  bpoly3  16024  bpoly4  16025  fsumcube  16026  ef4p  16081  ef01bndlem  16152  ge2nprmge4  16671  lt6abl  19825  cphipval  25143  sincosq4sgn  26410  binom4  26760  quart1lem  26765  log2cnv  26854  ppiublem2  27114  ppiub  27115  chtub  27123  bclbnd  27191  bposlem8  27202  lgsdir2lem3  27238  3wlkdlem1  30088  ipval2  30636  problem3  35654  aks4d1p1p7  42062  rmydioph  43003  rmxdioph  43005  expdiophlem2  43011  lt4addmuld  45304  stoweidlem13  46011  m1modnep2mod  47353  4even  47710  sbgoldbo  47788  ackval40  48682  ackval41a  48683  ackval42  48685