Theorem 7t2e14

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

	Ref	Expression
Assertion	7t2e14	⊢ ( 7 · 2 ) = ; 1 4

Proof

Step	Hyp	Ref	Expression
1		7cn	⊢ 7 ∈ ℂ
2	1	times2i	⊢ ( 7 · 2 ) = ( 7 + 7 )
3		7p7e14	⊢ ( 7 + 7 ) = ; 1 4
4	2 3	eqtri	⊢ ( 7 · 2 ) = ; 1 4