Definition df-5 12408

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 12400	. 2 class 5
2		c4 12399	. . 3 class 4
3		c1 11201	. . 3 class 1
4		caddc 11203	. . 3 class +
5	2, 3, 4	co 7420	. 2 class (4 + 1)
6	1, 5	wceq 1569	1 wff 5 = (4 + 1)

This definition is used by:  5nn  12429  5re  12430  5cn  12431  5m1e4  12472  4p1e5  12488  3p2e5  12493  4p2e6  12495  4lt5  12522  5p5e10  12890  6p5e11  12892  7p5e12  12896  8p5e13  12902  8p7e15  12904  9p5e14  12909  9p6e15  12910  5t5e25  12922  6t5e30  12926  7t5e35  12931  8t5e40  12937  9t5e45  12944  fldiv4p1lem1div2  13975  ef01bndlem  16352  prm23lt5  16992  5prm  17286  lt6abl  20109  log2ublem3  27276  ppiublem2  27530  bclbnd  27607  bposlem6  27616  bposlem9  27619  lgsdir2lem3  27654  2lgslem3c  27725  2lgsoddprmlem3c  27739  ex-exp  31051  ex-fac  31052  ex-bc  31053  3lexlogpow5ineq5  43111  aks4d1p1p7  43125  1p5e6  43313  4p5e9  43325  rmydioph  44021  expdiophlem2  44029  stoweidlem13  47023  cos5t  47925  goldpolyfactor  47927  goldratval  47936  fmtno5  48642  fmtnofac1  48655  31prm  48682  5odd  48808  sbgoldbo  48885  gpgprismgr4cycllem7  49199  gpgprismgr4cycllem9  49201  ackval50  49810