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