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 |
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 |