Definition df-5 12039

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 12031	. 2 class 5
2		c4 12030	. . 3 class 4
3		c1 10872	. . 3 class 1
4		caddc 10874	. . 3 class +
5	2, 3, 4	co 7275	. 2 class (4 + 1)
6	1, 5	wceq 1539	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12059  5re  12060  5cn  12061  5pos  12082  5m1e4  12103  4p1e5  12119  3p2e5  12124  4p2e6  12126  4lt5  12150  5p5e10  12508  6p5e11  12510  7p5e12  12514  8p5e13  12520  8p7e15  12522  9p5e14  12527  9p6e15  12528  5t5e25  12540  6t5e30  12544  7t5e35  12549  8t5e40  12555  9t5e45  12562  fldiv4p1lem1div2  13555  ef01bndlem  15893  prm23lt5  16515  5prm  16810  lt6abl  19496  log2ublem3  26098  ppiublem2  26351  bclbnd  26428  bposlem6  26437  bposlem9  26440  lgsdir2lem3  26475  2lgslem3c  26546  2lgsoddprmlem3c  26560  ex-exp  28814  ex-fac  28815  ex-bc  28816  3lexlogpow5ineq5  40068  aks4d1p1p7  40082  rmydioph  40836  expdiophlem2  40844  stoweidlem13  43554  fmtno5  45009  fmtnofac1  45022  31prm  45049  5odd  45162  sbgoldbo  45239  ackval50  46044