Definition df-5 12253

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 12245	. 2 class 5
2		c4 12244	. . 3 class 4
3		c1 11075	. . 3 class 1
4		caddc 11077	. . 3 class +
5	2, 3, 4	co 7389	. 2 class (4 + 1)
6	1, 5	wceq 1540	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12273  5re  12274  5cn  12275  5pos  12296  5m1e4  12317  4p1e5  12333  3p2e5  12338  4p2e6  12340  4lt5  12364  5p5e10  12726  6p5e11  12728  7p5e12  12732  8p5e13  12738  8p7e15  12740  9p5e14  12745  9p6e15  12746  5t5e25  12758  6t5e30  12762  7t5e35  12767  8t5e40  12773  9t5e45  12780  fldiv4p1lem1div2  13803  ef01bndlem  16158  prm23lt5  16791  5prm  17085  lt6abl  19831  log2ublem3  26864  ppiublem2  27120  bclbnd  27197  bposlem6  27206  bposlem9  27209  lgsdir2lem3  27244  2lgslem3c  27315  2lgsoddprmlem3c  27329  ex-exp  30385  ex-fac  30386  ex-bc  30387  3lexlogpow5ineq5  42043  aks4d1p1p7  42057  rmydioph  42996  expdiophlem2  43004  stoweidlem13  46004  fmtno5  47548  fmtnofac1  47561  31prm  47588  5odd  47701  sbgoldbo  47778  gpgprismgr4cycllem7  48081  gpgprismgr4cycllem9  48083  ackval50  48677