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