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 11067
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 11058 . 2 class 5
2 c4 11057 . . 3 class 4
3 c1 9922 . . 3 class 1
4 caddc 9924 . . 3 class +
52, 3, 4co 6635 . 2 class (4 + 1)
61, 5wceq 1481 1 wff 5 = (4 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  5re  11084  5pos  11103  5m1e4  11124  4p1e5  11139  3p2e5  11145  4p2e6  11147  5p5e10OLD  11153  5nn  11173  4lt5  11185  5p5e10  11581  6p5e11  11585  6p5e11OLD  11586  7p5e12  11592  8p5e13  11600  8p7e15  11602  9p5e14  11608  9p6e15  11609  5t5e25  11624  5t5e25OLD  11625  6t5e30  11629  6t5e30OLD  11630  7t5e35  11636  8t5e40  11642  8t5e40OLD  11643  9t5e45  11651  fldiv4p1lem1div2  12619  ef01bndlem  14895  prm23lt5  15500  5prm  15796  lt6abl  18277  log2ublem3  24656  ppiublem2  24909  bclbnd  24986  bposlem6  24995  bposlem9  24998  lgsdir2lem3  25033  2lgslem3c  25104  2lgsoddprmlem3c  25118  ex-exp  27277  ex-fac  27278  ex-bc  27279  rmydioph  37400  expdiophlem2  37408  stoweidlem13  39993  fmtno5  41234  fmtnofac1  41247  31prm  41277  5odd  41384  sbgoldbo  41440
  Copyright terms: Public domain W3C validator