Theorem addassnni

Description: Associative law for addition. (Contributed by metakunt, 25-Apr-2024)

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

Proof

Step	Hyp	Ref	Expression
1		addassnni.1	⊢ 𝐴 ∈ ℕ
2		addassnni.2	⊢ 𝐵 ∈ ℕ
3		addassnni.3	⊢ 𝐶 ∈ ℕ
4	1	nncni	⊢ 𝐴 ∈ ℂ
5	2	nncni	⊢ 𝐵 ∈ ℂ
6	3	nncni	⊢ 𝐶 ∈ ℂ
7	4 5 6	addassi	⊢ ( ( 𝐴 + 𝐵 ) + 𝐶 ) = ( 𝐴 + ( 𝐵 + 𝐶 ) )