Definition df-5 12331

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 12323	. 2 class 5
2		c4 12322	. . 3 class 4
3		c1 11126	. . 3 class 1
4		caddc 11128	. . 3 class +
5	2, 3, 4	co 7416	. 2 class (4 + 1)
6	1, 5	wceq 1570	1 wff 5 = (4 + 1)

This definition is used by:  5nn  12352  5re  12353  5cn  12354  5m1e4  12395  4p1e5  12411  3p2e5  12416  4p2e6  12418  4lt5  12445  5p5e10  12813  6p5e11  12815  7p5e12  12819  8p5e13  12825  8p7e15  12827  9p5e14  12832  9p6e15  12833  5t5e25  12845  6t5e30  12849  7t5e35  12854  8t5e40  12860  9t5e45  12867  fldiv4p1lem1div2  13896  ef01bndlem  16274  prm23lt5  16908  5prm  17202  lt6abl  20021  log2ublem3  27181  ppiublem2  27435  bclbnd  27512  bposlem6  27521  bposlem9  27524  lgsdir2lem3  27559  2lgslem3c  27630  2lgsoddprmlem3c  27644  ex-exp  30914  ex-fac  30915  ex-bc  30916  3lexlogpow5ineq5  42911  aks4d1p1p7  42925  1p5e6  43113  4p5e9  43125  rmydioph  43840  expdiophlem2  43848  stoweidlem13  46826  cos5t  47728  goldpolyfactor  47730  goldratval  47739  fmtno5  48445  fmtnofac1  48458  31prm  48485  5odd  48611  sbgoldbo  48688  gpgprismgr4cycllem7  49002  gpgprismgr4cycllem9  49004  ackval50  49613