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

Metamath Proof Explorer

Theorem 3t2e6

Description: 3 times 2 equals 6. (Contributed by NM, 2-Aug-2004)

		Ref	Expression
	Assertion	3t2e6	$⊢ 3 \cdot 2 = 6$

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