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

Metamath Proof Explorer

Theorem mullidi

Description: Identity law for multiplication. (Contributed by NM, 14-Feb-1995)

		Ref	Expression
	Hypothesis	axi.1	$⊢ A \in ℂ$
	Assertion	mullidi	$⊢ 1 A = A$

Step	Hyp	Ref	Expression
1		axi.1	$⊢ A \in ℂ$
2		mullid	$⊢ A \in ℂ \to 1 A = A$
3	1 2	ax-mp	$⊢ 1 A = A$