Definition df-5 12215

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 12207	. 2 class 5
2		c4 12206	. . 3 class 4
3		c1 11031	. . 3 class 1
4		caddc 11033	. . 3 class +
5	2, 3, 4	co 7360	. 2 class (4 + 1)
6	1, 5	wceq 1542	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12235  5re  12236  5cn  12237  5pos  12258  5m1e4  12274  4p1e5  12290  3p2e5  12295  4p2e6  12297  4lt5  12321  5p5e10  12682  6p5e11  12684  7p5e12  12688  8p5e13  12694  8p7e15  12696  9p5e14  12701  9p6e15  12702  5t5e25  12714  6t5e30  12718  7t5e35  12723  8t5e40  12729  9t5e45  12736  fldiv4p1lem1div2  13759  ef01bndlem  16113  prm23lt5  16746  5prm  17040  lt6abl  19828  log2ublem3  26918  ppiublem2  27174  bclbnd  27251  bposlem6  27260  bposlem9  27263  lgsdir2lem3  27298  2lgslem3c  27369  2lgsoddprmlem3c  27383  ex-exp  30529  ex-fac  30530  ex-bc  30531  3lexlogpow5ineq5  42382  aks4d1p1p7  42396  rmydioph  43323  expdiophlem2  43331  stoweidlem13  46324  fmtno5  47870  fmtnofac1  47883  31prm  47910  5odd  48023  sbgoldbo  48100  gpgprismgr4cycllem7  48414  gpgprismgr4cycllem9  48416  ackval50  49011