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 11706
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 11698 . 2 class 5
2 c4 11697 . . 3 class 4
3 c1 10541 . . 3 class 1
4 caddc 10543 . . 3 class +
52, 3, 4co 7159 . 2 class (4 + 1)
61, 5wceq 1536 1 wff 5 = (4 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  5nn  11726  5re  11727  5cn  11728  5pos  11749  5m1e4  11770  4p1e5  11786  3p2e5  11791  4p2e6  11793  4lt5  11817  5p5e10  12172  6p5e11  12174  7p5e12  12178  8p5e13  12184  8p7e15  12186  9p5e14  12191  9p6e15  12192  5t5e25  12204  6t5e30  12208  7t5e35  12213  8t5e40  12219  9t5e45  12226  fldiv4p1lem1div2  13208  ef01bndlem  15540  prm23lt5  16154  5prm  16445  lt6abl  19018  log2ublem3  25529  ppiublem2  25782  bclbnd  25859  bposlem6  25868  bposlem9  25871  lgsdir2lem3  25906  2lgslem3c  25977  2lgsoddprmlem3c  25991  ex-exp  28232  ex-fac  28233  ex-bc  28234  rmydioph  39617  expdiophlem2  39625  stoweidlem13  42305  fmtno5  43726  fmtnofac1  43739  31prm  43767  5odd  43882  sbgoldbo  43959
  Copyright terms: Public domain W3C validator