MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-5 Structured version   Visualization version   GIF version

Definition df-5 10929
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
StepHypRef Expression
1 c5 10920 . 2 class 5
2 c4 10919 . . 3 class 4
3 c1 9793 . . 3 class 1
4 caddc 9795 . . 3 class +
52, 3, 4co 6527 . 2 class (4 + 1)
61, 5wceq 1474 1 wff 5 = (4 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  5re  10946  5pos  10965  5m1e4  10986  4p1e5  11001  3p2e5  11007  4p2e6  11009  5p5e10OLD  11015  5nn  11035  4lt5  11047  5p5e10  11428  6p5e11  11432  6p5e11OLD  11433  7p5e12  11439  8p5e13  11447  8p7e15  11449  9p5e14  11455  9p6e15  11456  5t5e25  11471  5t5e25OLD  11472  6t5e30  11476  6t5e30OLD  11477  7t5e35  11483  8t5e40  11489  8t5e40OLD  11490  9t5e45  11498  fldiv4p1lem1div2  12453  ef01bndlem  14699  prm23lt5  15303  5prm  15599  lt6abl  18065  log2ublem3  24392  ppiublem2  24645  bclbnd  24722  bposlem6  24731  bposlem9  24734  lgsdir2lem3  24769  2lgslem3c  24840  2lgsoddprmlem3c  24854  ex-exp  26465  ex-fac  26466  ex-bc  26467  rmydioph  36402  expdiophlem2  36410  stoweidlem13  38710  fmtno5  39812  fmtnofac1  39825  31prm  39855  5odd  39962
  Copyright terms: Public domain W3C validator