Definition df-5 12228

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 12220	. 2 class 5
2		c4 12219	. . 3 class 4
3		c1 11045	. . 3 class 1
4		caddc 11047	. . 3 class +
5	2, 3, 4	co 7369	. 2 class (4 + 1)
6	1, 5	wceq 1540	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12248  5re  12249  5cn  12250  5pos  12271  5m1e4  12287  4p1e5  12303  3p2e5  12308  4p2e6  12310  4lt5  12334  5p5e10  12696  6p5e11  12698  7p5e12  12702  8p5e13  12708  8p7e15  12710  9p5e14  12715  9p6e15  12716  5t5e25  12728  6t5e30  12732  7t5e35  12737  8t5e40  12743  9t5e45  12750  fldiv4p1lem1div2  13773  ef01bndlem  16128  prm23lt5  16761  5prm  17055  lt6abl  19801  log2ublem3  26834  ppiublem2  27090  bclbnd  27167  bposlem6  27176  bposlem9  27179  lgsdir2lem3  27214  2lgslem3c  27285  2lgsoddprmlem3c  27299  ex-exp  30352  ex-fac  30353  ex-bc  30354  3lexlogpow5ineq5  42021  aks4d1p1p7  42035  rmydioph  42976  expdiophlem2  42984  stoweidlem13  45984  fmtno5  47531  fmtnofac1  47544  31prm  47571  5odd  47684  sbgoldbo  47761  gpgprismgr4cycllem7  48064  gpgprismgr4cycllem9  48066  ackval50  48660