Theorem 2txmxeqx

Description: Two times a complex number minus the number itself results in the number itself. (Contributed by Alexander van der Vekens, 8-Jun-2018)

	Ref	Expression
Assertion	2txmxeqx	$$⊢X\in ℂ\to 2X-X=X$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢X\in ℂ\to X\in ℂ$$
2		2times	$$⊢X\in ℂ\to 2X=X+X$$
3	1 1 2	mvrladdd	$$⊢X\in ℂ\to 2X-X=X$$