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

Metamath Proof Explorer

Theorem mullid

Description: Identity law for multiplication. See mulrid for commuted version. (Contributed by NM, 8-Oct-1999)

		Ref	Expression
	Assertion	mullid	$⊢ A \in ℂ \to 1 A = A$

Step	Hyp	Ref	Expression
1		ax-1cn	$⊢ 1 \in ℂ$
2		mulcom	$⊢ (1 \in ℂ \land A \in ℂ) \to 1 A = A \cdot 1$
3	1 2	mpan	$⊢ A \in ℂ \to 1 A = A \cdot 1$
4		mulrid	$⊢ A \in ℂ \to A \cdot 1 = A$
5	3 4	eqtrd	$⊢ A \in ℂ \to 1 A = A$