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 · 1 ) = i

Proof

Step	Hyp	Ref	Expression
1		sn-1ticom	⊢ ( 1 · i ) = ( i · 1 )
2		ax-icn	⊢ i ∈ ℂ
3		sn-mullid	⊢ ( i ∈ ℂ → ( 1 · i ) = i )
4	2 3	ax-mp	⊢ ( 1 · i ) = i
5	1 4	eqtr3i	⊢ ( i · 1 ) = i