Definition df-5 12191

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 12183	. 2 class 5
2		c4 12182	. . 3 class 4
3		c1 11007	. . 3 class 1
4		caddc 11009	. . 3 class +
5	2, 3, 4	co 7346	. 2 class (4 + 1)
6	1, 5	wceq 1541	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12211  5re  12212  5cn  12213  5pos  12234  5m1e4  12250  4p1e5  12266  3p2e5  12271  4p2e6  12273  4lt5  12297  5p5e10  12659  6p5e11  12661  7p5e12  12665  8p5e13  12671  8p7e15  12673  9p5e14  12678  9p6e15  12679  5t5e25  12691  6t5e30  12695  7t5e35  12700  8t5e40  12706  9t5e45  12713  fldiv4p1lem1div2  13739  ef01bndlem  16093  prm23lt5  16726  5prm  17020  lt6abl  19807  log2ublem3  26885  ppiublem2  27141  bclbnd  27218  bposlem6  27227  bposlem9  27230  lgsdir2lem3  27265  2lgslem3c  27336  2lgsoddprmlem3c  27350  ex-exp  30430  ex-fac  30431  ex-bc  30432  3lexlogpow5ineq5  42163  aks4d1p1p7  42177  rmydioph  43117  expdiophlem2  43125  stoweidlem13  46121  fmtno5  47667  fmtnofac1  47680  31prm  47707  5odd  47820  sbgoldbo  47897  gpgprismgr4cycllem7  48211  gpgprismgr4cycllem9  48213  ackval50  48809