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

Definition df-7 10377
Description: Define the number 7. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-7

Detailed syntax breakdown of Definition df-7
StepHypRef Expression
1 c7 10368 . 2
2 c6 10367 . . 3
3 c1 9275 . . 3
4 caddc 9277 . . 3
52, 3, 4co 6086 . 2
61, 5wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  7re  10396  7pos  10413  6p1e7  10442  4p3e7  10449  5p2e7  10451  6p2e8  10455  7nn  10476  6lt7  10495  7p7e14  10802  8p7e15  10807  9p7e16  10814  9p8e17  10815  7t7e49  10834  8t7e56  10840  9t7e63  10847  7prm  14130  17prm  14136  37prm  14140  317prm  14145  log2ublem2  22322  log2ublem3  22323  bclbnd  22599  bposlem8  22610  lgsdir2lem3  22644  problem4  27270  rmydioph  29334  expdiophlem2  29342
  Copyright terms: Public domain W3C validator