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

Metamath Proof Explorer

Theorem 1p1times

Description: Two times a number. (Contributed by NM, 18-May-1999) (Revised by Mario Carneiro, 27-May-2016)

		Ref	Expression
	Assertion	1p1times	$⊢ A \in ℂ \to (1 + 1) A = A + A$

Step	Hyp	Ref	Expression
1		1cnd	$⊢ A \in ℂ \to 1 \in ℂ$
2		id	$⊢ A \in ℂ \to A \in ℂ$
3		mullid	$⊢ A \in ℂ \to 1 A = A$
4	3 3	oveq12d	$⊢ A \in ℂ \to 1 A + 1 A = A + A$
5	1 2 1 4	joinlmuladdmuld	$⊢ A \in ℂ \to (1 + 1) A = A + A$