Metamath Proof Explorer

Theorem nnasuc

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

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

Proof

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