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

Metamath Proof Explorer

Theorem sn-it1ei

Description: it1ei without ax-mulcom . (See sn-mullid for commuted version). (Contributed by SN, 1-Jun-2024)

		Ref	Expression
	Assertion	sn-it1ei	$⊢ i \cdot 1 = i$

Step	Hyp	Ref	Expression
1		sn-1ticom	$⊢ 1 i = i \cdot 1$
2		ax-icn	$⊢ i \in ℂ$
3		sn-mullid	$⊢ i \in ℂ \to 1 i = i$
4	2 3	ax-mp	$⊢ 1 i = i$
5	1 4	eqtr3i	$⊢ i \cdot 1 = i$