Theorem naddcld

Description: Closure law for natural addition. Deduction version. (Contributed by Scott Fenton, 10-Jun-2025)

	Ref	Expression
Hypotheses	naddcld.1	$$⊢\phi \to A\in \mathrm{On}$$
	naddcld.2	$$⊢\phi \to B\in \mathrm{On}$$
Assertion	naddcld	$$⊢\phi \to A+B\in \mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		naddcld.1	$$⊢\phi \to A\in \mathrm{On}$$
2		naddcld.2	$$⊢\phi \to B\in \mathrm{On}$$
3		naddcl	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to A+B\in \mathrm{On}$$
4	1 2 3	syl2anc	$$⊢\phi \to A+B\in \mathrm{On}$$