Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Arithmetic theorems
2p6e8
Next ⟩
2p7e9
Metamath Proof Explorer
Ascii
Unicode
Theorem
2p6e8
Description:
2 + 6 = 8.
(Contributed by
SN
, 24-Aug-2026)
Ref
Expression
Assertion
2p6e8
⊢
2
+
6
=
8
Proof
Step
Hyp
Ref
Expression
1
2cn
⊢
2
∈
ℂ
2
4cn
⊢
4
∈
ℂ
3
1
1
2
addassi
⊢
2
+
2
+
4
=
2
+
2
+
4
4
2p2e4
⊢
2
+
2
=
4
5
4
oveq1i
⊢
2
+
2
+
4
=
4
+
4
6
4p4e8
⊢
4
+
4
=
8
7
5
6
eqtri
⊢
2
+
2
+
4
=
8
8
2p4e6
⊢
2
+
4
=
6
9
8
oveq2i
⊢
2
+
2
+
4
=
2
+
6
10
3
7
9
3eqtr3ri
⊢
2
+
6
=
8