Metamath Proof Explorer

Theorem nnmsuc

Description: Multiplication with successor. Theorem 4J(A2) of Enderton p. 80. (Contributed by NM, 20-Sep-1995) (Revised by Mario Carneiro, 14-Nov-2014)

Ref Expression
Assertion nnmsuc 
|- ( ( A e. _om /\ B e. _om ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) )

Proof

Step Hyp Ref Expression
1 nnon 
 |-  ( A e. _om -> A e. On )
2 onmsuc 
 |-  ( ( A e. On /\ B e. _om ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) )
3 1 2 sylan 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) )