Theorem nn0addcli

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

	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