Theorem times2

Description: A number times 2. (Contributed by NM, 16-Oct-2007)

	Ref	Expression
Assertion	times2	$$⊢A\in ℂ\to A\cdot 2=A+A$$

Proof

Step	Hyp	Ref	Expression
1		2cn	$$⊢2\in ℂ$$
2		mulcom	$$⊢\left(A\in ℂ\wedge 2\in ℂ\right)\to A\cdot 2=2A$$
3	1 2	mpan2	$$⊢A\in ℂ\to A\cdot 2=2A$$
4		2times	$$⊢A\in ℂ\to 2A=A+A$$
5	3 4	eqtrd	$$⊢A\in ℂ\to A\cdot 2=A+A$$