Definition df-5 12282

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 12274	. 2 class 5
2		c4 12273	. . 3 class 4
3		c1 11113	. . 3 class 1
4		caddc 11115	. . 3 class +
5	2, 3, 4	co 7405	. 2 class (4 + 1)
6	1, 5	wceq 1533	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12302  5re  12303  5cn  12304  5pos  12325  5m1e4  12346  4p1e5  12362  3p2e5  12367  4p2e6  12369  4lt5  12393  5p5e10  12752  6p5e11  12754  7p5e12  12758  8p5e13  12764  8p7e15  12766  9p5e14  12771  9p6e15  12772  5t5e25  12784  6t5e30  12788  7t5e35  12793  8t5e40  12799  9t5e45  12806  fldiv4p1lem1div2  13806  ef01bndlem  16134  prm23lt5  16756  5prm  17051  lt6abl  19815  log2ublem3  26835  ppiublem2  27091  bclbnd  27168  bposlem6  27177  bposlem9  27180  lgsdir2lem3  27215  2lgslem3c  27286  2lgsoddprmlem3c  27300  ex-exp  30212  ex-fac  30213  ex-bc  30214  3lexlogpow5ineq5  41442  aks4d1p1p7  41456  rmydioph  42336  expdiophlem2  42344  stoweidlem13  45306  fmtno5  46802  fmtnofac1  46815  31prm  46842  5odd  46955  sbgoldbo  47032  ackval50  47664