Metamath Proof Explorer


Theorem 7t2e14

Description: 7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015)

Ref Expression
Assertion 7t2e14 ⊢ 7 ⋅ 2 = 14

Proof

Step Hyp Ref Expression
1 7cn ⊢ 7 ∈ ℂ
2 1 times2i ⊢ 7 ⋅ 2 = 7 + 7
3 7p7e14 ⊢ 7 + 7 = 14
4 2 3 eqtri ⊢ 7 ⋅ 2 = 14