Definition df-5 12225

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 12217	. 2 class 5
2		c4 12216	. . 3 class 4
3		c1 11041	. . 3 class 1
4		caddc 11043	. . 3 class +
5	2, 3, 4	co 7370	. 2 class (4 + 1)
6	1, 5	wceq 1542	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12245  5re  12246  5cn  12247  5pos  12268  5m1e4  12284  4p1e5  12300  3p2e5  12305  4p2e6  12307  4lt5  12331  5p5e10  12692  6p5e11  12694  7p5e12  12698  8p5e13  12704  8p7e15  12706  9p5e14  12711  9p6e15  12712  5t5e25  12724  6t5e30  12728  7t5e35  12733  8t5e40  12739  9t5e45  12746  fldiv4p1lem1div2  13769  ef01bndlem  16123  prm23lt5  16756  5prm  17050  lt6abl  19841  log2ublem3  26931  ppiublem2  27187  bclbnd  27264  bposlem6  27273  bposlem9  27276  lgsdir2lem3  27311  2lgslem3c  27382  2lgsoddprmlem3c  27396  ex-exp  30543  ex-fac  30544  ex-bc  30545  3lexlogpow5ineq5  42459  aks4d1p1p7  42473  rmydioph  43400  expdiophlem2  43408  stoweidlem13  46400  fmtno5  47946  fmtnofac1  47959  31prm  47986  5odd  48099  sbgoldbo  48176  gpgprismgr4cycllem7  48490  gpgprismgr4cycllem9  48492  ackval50  49087