Theorem 6t2e12

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

	Ref	Expression
Assertion	6t2e12	⊢ ( 6 · 2 ) = ; 1 2

Proof

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