Theorem nnaddcomli

Description: Version of addcomli for natural numbers. (Contributed by Steven Nguyen, 1-Aug-2023)

	Ref	Expression
Hypotheses	nnaddcomli.1	$$⊢A\in \mathbb{N}$$
	nnaddcomli.2	$$⊢B\in \mathbb{N}$$
	nnaddcomli.3	$$⊢A+B=C$$
Assertion	nnaddcomli	$$⊢B+A=C$$

Proof

Step	Hyp	Ref	Expression
1		nnaddcomli.1	$$⊢A\in \mathbb{N}$$
2		nnaddcomli.2	$$⊢B\in \mathbb{N}$$
3		nnaddcomli.3	$$⊢A+B=C$$
4		nnaddcom	$$⊢\left(B\in \mathbb{N}\wedge A\in \mathbb{N}\right)\to B+A=A+B$$
5	2 1 4	mp2an	$$⊢B+A=A+B$$
6	5 3	eqtri	$$⊢B+A=C$$