Definition df-5 12304

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 12296	. 2 class 5
2		c4 12295	. . 3 class 4
3		c1 11128	. . 3 class 1
4		caddc 11130	. . 3 class +
5	2, 3, 4	co 7403	. 2 class (4 + 1)
6	1, 5	wceq 1540	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12324  5re  12325  5cn  12326  5pos  12347  5m1e4  12368  4p1e5  12384  3p2e5  12389  4p2e6  12391  4lt5  12415  5p5e10  12777  6p5e11  12779  7p5e12  12783  8p5e13  12789  8p7e15  12791  9p5e14  12796  9p6e15  12797  5t5e25  12809  6t5e30  12813  7t5e35  12818  8t5e40  12824  9t5e45  12831  fldiv4p1lem1div2  13850  ef01bndlem  16200  prm23lt5  16832  5prm  17126  lt6abl  19874  log2ublem3  26908  ppiublem2  27164  bclbnd  27241  bposlem6  27250  bposlem9  27253  lgsdir2lem3  27288  2lgslem3c  27359  2lgsoddprmlem3c  27373  ex-exp  30377  ex-fac  30378  ex-bc  30379  3lexlogpow5ineq5  42019  aks4d1p1p7  42033  rmydioph  42985  expdiophlem2  42993  stoweidlem13  45990  fmtno5  47519  fmtnofac1  47532  31prm  47559  5odd  47672  sbgoldbo  47749  gpgprismgr4cycllem7  48048  gpgprismgr4cycllem9  48050  ackval50  48626