This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 6t2e12

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

		Ref	Expression
	Assertion	6t2e12	$⊢ 6 \cdot 2 = 12$

Step	Hyp	Ref	Expression
1		6cn	$⊢ 6 \in ℂ$
2	1	times2i	$⊢ 6 \cdot 2 = 6 + 6$
3		6p6e12	$⊢ 6 + 6 = 12$
4	2 3	eqtri	$⊢ 6 \cdot 2 = 12$