Metamath Proof Explorer


Theorem nnaddcomli

Description: Version of addcomli for natural numbers. (Contributed by Steven Nguyen, 1-Aug-2023)

Ref Expression
Hypotheses nnaddcomli.1
|- A e. NN
nnaddcomli.2
|- B e. NN
nnaddcomli.3
|- ( A + B ) = C
Assertion nnaddcomli
|- ( B + A ) = C

Proof

Step Hyp Ref Expression
1 nnaddcomli.1
 |-  A e. NN
2 nnaddcomli.2
 |-  B e. NN
3 nnaddcomli.3
 |-  ( A + B ) = C
4 nnaddcom
 |-  ( ( B e. NN /\ A e. NN ) -> ( B + A ) = ( A + B ) )
5 2 1 4 mp2an
 |-  ( B + A ) = ( A + B )
6 5 3 eqtri
 |-  ( B + A ) = C