Database
REAL AND COMPLEX NUMBERS
Integer sets
Decimal arithmetic
6t2e12
Next ⟩
6t3e18
Metamath Proof Explorer
Ascii
Unicode
Theorem
6t2e12
Description:
6 times 2 equals 12.
(Contributed by
Mario Carneiro
, 19-Apr-2015)
Ref
Expression
Assertion
6t2e12
⊢
6
⋅
2
=
12
Proof
Step
Hyp
Ref
Expression
1
6cn
⊢
6
∈
ℂ
2
1
times2i
⊢
6
⋅
2
=
6
+
6
3
6p6e12
⊢
6
+
6
=
12
4
2
3
eqtri
⊢
6
⋅
2
=
12