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