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

Definition df-7 12334
Description: Define the number 7. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-7 7 = (6 + 1)

Detailed syntax breakdown of Definition df-7
StepHypRef Expression
1 c7 12326 . 2 class 7
2 c6 12325 . . 3 class 6
3 c1 11156 . . 3 class 1
4 caddc 11158 . . 3 class +
52, 3, 4co 7431 . 2 class (6 + 1)
61, 5wceq 1540 1 wff 7 = (6 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  7nn  12358  7re  12359  7cn  12360  7pos  12377  7m1e6  12398  6p1e7  12414  4p3e7  12420  5p2e7  12422  6p2e8  12425  6lt7  12452  7p7e14  12812  8p7e15  12818  9p7e16  12825  9p8e17  12826  7t7e49  12847  8t7e56  12853  9t7e63  12860  2exp7  17125  7prm  17148  17prm  17154  37prm  17158  317prm  17163  log2ublem2  26990  log2ublem3  26991  bclbnd  27324  bposlem8  27335  lgsdir2lem3  27371  problem4  35673  3cubeslem3r  42698  rmydioph  43026  expdiophlem2  43034  fmtno5  47544  257prm  47548  127prm  47586  7odd  47699  stgoldbwt  47763
  Copyright terms: Public domain W3C validator