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

Metamath Proof Explorer

Theorem 4t2e8

Description: 4 times 2 equals 8. (Contributed by NM, 2-Aug-2004)

		Ref	Expression
	Assertion	4t2e8	$⊢ 4 \cdot 2 = 8$

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