Metamath Proof Explorer
Description: Closure of addition of nonnegative integers, inference form.
(Contributed by Raph Levien, 10Dec2002)


Ref 
Expression 

Hypotheses 
nn0addcli.1 
⊢ 𝑀 ∈ ℕ_{0} 


nn0addcli.2 
⊢ 𝑁 ∈ ℕ_{0} 

Assertion 
nn0addcli 
⊢ ( 𝑀 + 𝑁 ) ∈ ℕ_{0} 
Proof
Step 
Hyp 
Ref 
Expression 
1 

nn0addcli.1 
⊢ 𝑀 ∈ ℕ_{0} 
2 

nn0addcli.2 
⊢ 𝑁 ∈ ℕ_{0} 
3 

nn0addcl 
⊢ ( ( 𝑀 ∈ ℕ_{0} ∧ 𝑁 ∈ ℕ_{0} ) → ( 𝑀 + 𝑁 ) ∈ ℕ_{0} ) 
4 
1 2 3

mp2an 
⊢ ( 𝑀 + 𝑁 ) ∈ ℕ_{0} 