Theorem nnaddcomli

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

	Ref	Expression
Hypotheses	nnaddcomli.1	⊢ 𝐴 ∈ ℕ
	nnaddcomli.2	⊢ 𝐵 ∈ ℕ
	nnaddcomli.3	⊢ ( 𝐴 + 𝐵 ) = 𝐶
Assertion	nnaddcomli	⊢ ( 𝐵 + 𝐴 ) = 𝐶

Proof

Step	Hyp	Ref	Expression
1		nnaddcomli.1	⊢ 𝐴 ∈ ℕ
2		nnaddcomli.2	⊢ 𝐵 ∈ ℕ
3		nnaddcomli.3	⊢ ( 𝐴 + 𝐵 ) = 𝐶
4		nnaddcom	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐴 ∈ ℕ ) → ( 𝐵 + 𝐴 ) = ( 𝐴 + 𝐵 ) )
5	2 1 4	mp2an	⊢ ( 𝐵 + 𝐴 ) = ( 𝐴 + 𝐵 )
6	5 3	eqtri	⊢ ( 𝐵 + 𝐴 ) = 𝐶