Metamath Proof Explorer

Theorem nmullid

Description: Identity law for natural multiplication. (Contributed by Scott Fenton, 21-Jul-2026)

Ref Expression
Assertion nmullid 
|- ( A e. On -> ( 1o .no A ) = A )

Proof

Step Hyp Ref Expression
1 1on 
 |-  1o e. On
2 nmulcom 
 |-  ( ( 1o e. On /\ A e. On ) -> ( 1o .no A ) = ( A .no 1o ) )
3 1 2 mpan 
 |-  ( A e. On -> ( 1o .no A ) = ( A .no 1o ) )
4 nmulrid 
 |-  ( A e. On -> ( A .no 1o ) = A )
5 3 4 eqtrd 
 |-  ( A e. On -> ( 1o .no A ) = A )