Definition df-5 12305

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 12297	. 2 class 5
2		c4 12296	. . 3 class 4
3		c1 11100	. . 3 class 1
4		caddc 11102	. . 3 class +
5	2, 3, 4	co 7410	. 2 class (4 + 1)
6	1, 5	wceq 1568	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12326  5re  12327  5cn  12328  5m1e4  12369  4p1e5  12385  3p2e5  12390  4p2e6  12392  4lt5  12419  5p5e10  12786  6p5e11  12788  7p5e12  12792  8p5e13  12798  8p7e15  12800  9p5e14  12805  9p6e15  12806  5t5e25  12818  6t5e30  12822  7t5e35  12827  8t5e40  12833  9t5e45  12840  fldiv4p1lem1div2  13867  ef01bndlem  16239  prm23lt5  16873  5prm  17167  lt6abl  19964  log2ublem3  27089  ppiublem2  27343  bclbnd  27420  bposlem6  27429  bposlem9  27432  lgsdir2lem3  27467  2lgslem3c  27538  2lgsoddprmlem3c  27552  ex-exp  30767  ex-fac  30768  ex-bc  30769  3lexlogpow5ineq5  42773  aks4d1p1p7  42787  rmydioph  43689  expdiophlem2  43697  stoweidlem13  46675  cos5t  47561  fmtno5  48254  fmtnofac1  48267  31prm  48294  5odd  48420  sbgoldbo  48497  gpgprismgr4cycllem7  48811  gpgprismgr4cycllem9  48813  ackval50  49423