Database
REAL AND COMPLEX NUMBERS
Integer sets
Some properties of specific numbers
6p1e7
Next ⟩
7p1e8
Metamath Proof Explorer
Ascii
Unicode
Theorem
6p1e7
Description:
6 + 1 = 7.
(Contributed by
Mario Carneiro
, 18-Apr-2015)
Ref
Expression
Assertion
6p1e7
⊢
6
+
1
=
7
Proof
Step
Hyp
Ref
Expression
1
df-7
⊢
7
=
6
+
1
2
1
eqcomi
⊢
6
+
1
=
7