Metamath Proof Explorer


Theorem nn0addcli

Description: Closure of addition of nonnegative integers, inference form. (Contributed by Raph Levien, 10-Dec-2002)

Ref Expression
Hypotheses nn0addcli.1
|- M e. NN0
nn0addcli.2
|- N e. NN0
Assertion nn0addcli
|- ( M + N ) e. NN0

Proof

Step Hyp Ref Expression
1 nn0addcli.1
 |-  M e. NN0
2 nn0addcli.2
 |-  N e. NN0
3 nn0addcl
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M + N ) e. NN0 )
4 1 2 3 mp2an
 |-  ( M + N ) e. NN0