Theorem 4t2e8

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

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

Proof

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$$