Definition df-5 12209

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 12201	. 2 class 5
2		c4 12200	. . 3 class 4
3		c1 11025	. . 3 class 1
4		caddc 11027	. . 3 class +
5	2, 3, 4	co 7356	. 2 class (4 + 1)
6	1, 5	wceq 1541	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12229  5re  12230  5cn  12231  5pos  12252  5m1e4  12268  4p1e5  12284  3p2e5  12289  4p2e6  12291  4lt5  12315  5p5e10  12676  6p5e11  12678  7p5e12  12682  8p5e13  12688  8p7e15  12690  9p5e14  12695  9p6e15  12696  5t5e25  12708  6t5e30  12712  7t5e35  12717  8t5e40  12723  9t5e45  12730  fldiv4p1lem1div2  13753  ef01bndlem  16107  prm23lt5  16740  5prm  17034  lt6abl  19822  log2ublem3  26912  ppiublem2  27168  bclbnd  27245  bposlem6  27254  bposlem9  27257  lgsdir2lem3  27292  2lgslem3c  27363  2lgsoddprmlem3c  27377  ex-exp  30474  ex-fac  30475  ex-bc  30476  3lexlogpow5ineq5  42253  aks4d1p1p7  42267  rmydioph  43198  expdiophlem2  43206  stoweidlem13  46199  fmtno5  47745  fmtnofac1  47758  31prm  47785  5odd  47898  sbgoldbo  47975  gpgprismgr4cycllem7  48289  gpgprismgr4cycllem9  48291  ackval50  48886