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 · 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