Definition df-5 12194

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 12186	. 2 class 5
2		c4 12185	. . 3 class 4
3		c1 11010	. . 3 class 1
4		caddc 11012	. . 3 class +
5	2, 3, 4	co 7349	. 2 class (4 + 1)
6	1, 5	wceq 1540	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12214  5re  12215  5cn  12216  5pos  12237  5m1e4  12253  4p1e5  12269  3p2e5  12274  4p2e6  12276  4lt5  12300  5p5e10  12662  6p5e11  12664  7p5e12  12668  8p5e13  12674  8p7e15  12676  9p5e14  12681  9p6e15  12682  5t5e25  12694  6t5e30  12698  7t5e35  12703  8t5e40  12709  9t5e45  12716  fldiv4p1lem1div2  13739  ef01bndlem  16093  prm23lt5  16726  5prm  17020  lt6abl  19774  log2ublem3  26856  ppiublem2  27112  bclbnd  27189  bposlem6  27198  bposlem9  27201  lgsdir2lem3  27236  2lgslem3c  27307  2lgsoddprmlem3c  27321  ex-exp  30394  ex-fac  30395  ex-bc  30396  3lexlogpow5ineq5  42043  aks4d1p1p7  42057  rmydioph  42997  expdiophlem2  43005  stoweidlem13  46004  fmtno5  47551  fmtnofac1  47564  31prm  47591  5odd  47704  sbgoldbo  47781  gpgprismgr4cycllem7  48095  gpgprismgr4cycllem9  48097  ackval50  48693