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 x. 1 ) = _i

Proof

Step Hyp Ref Expression
1 sn-1ticom 
 |-  ( 1 x. _i ) = ( _i x. 1 )
2 ax-icn 
 |-  _i e. CC
3 sn-mullid 
 |-  ( _i e. CC -> ( 1 x. _i ) = _i )
4 2 3 ax-mp 
 |-  ( 1 x. _i ) = _i
5 1 4 eqtr3i 
 |-  ( _i x. 1 ) = _i