Definition df-5 12228

Description: Define the number 5. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
df-5	⊢ 5 = (4 + 1)

Detailed syntax breakdown of Definition df-5

Step	Hyp	Ref	Expression
1		c5 12220	. 2 class 5
2		c4 12219	. . 3 class 4
3		c1 11045	. . 3 class 1
4		caddc 11047	. . 3 class +
5	2, 3, 4	co 7369	. 2 class (4 + 1)
6	1, 5	wceq 1540	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12248  5re  12249  5cn  12250  5pos  12271  5m1e4  12287  4p1e5  12303  3p2e5  12308  4p2e6  12310  4lt5  12334  5p5e10  12696  6p5e11  12698  7p5e12  12702  8p5e13  12708  8p7e15  12710  9p5e14  12715  9p6e15  12716  5t5e25  12728  6t5e30  12732  7t5e35  12737  8t5e40  12743  9t5e45  12750  fldiv4p1lem1div2  13773  ef01bndlem  16128  prm23lt5  16761  5prm  17055  lt6abl  19809  log2ublem3  26891  ppiublem2  27147  bclbnd  27224  bposlem6  27233  bposlem9  27236  lgsdir2lem3  27271  2lgslem3c  27342  2lgsoddprmlem3c  27356  ex-exp  30429  ex-fac  30430  ex-bc  30431  3lexlogpow5ineq5  42041  aks4d1p1p7  42055  rmydioph  42996  expdiophlem2  43004  stoweidlem13  46004  fmtno5  47551  fmtnofac1  47564  31prm  47591  5odd  47704  sbgoldbo  47781  gpgprismgr4cycllem7  48084  gpgprismgr4cycllem9  48086  ackval50  48680