Database
REAL AND COMPLEX NUMBERS
Integer sets
Decimal arithmetic
6p6e12
Next ⟩
7p3e10
Metamath Proof Explorer
Ascii
Unicode
Theorem
6p6e12
Description:
6 + 6 = 12.
(Contributed by
Mario Carneiro
, 19-Apr-2015)
Ref
Expression
Assertion
6p6e12
⊢
6
+
6
=
12
Proof
Step
Hyp
Ref
Expression
1
6nn0
⊢
6
∈
ℕ
0
2
5nn0
⊢
5
∈
ℕ
0
3
1nn0
⊢
1
∈
ℕ
0
4
df-6
⊢
6
=
5
+
1
5
df-2
⊢
2
=
1
+
1
6
6p5e11
⊢
6
+
5
=
11
7
1
2
3
4
5
6
6p5lem
⊢
6
+
6
=
12