Theorem mulassnni

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

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

Proof

Step	Hyp	Ref	Expression
1		mulassnni.1	⊢ 𝐴 ∈ ℕ
2		mulassnni.2	⊢ 𝐵 ∈ ℕ
3		mulassnni.3	⊢ 𝐶 ∈ ℕ
4	1	nncni	⊢ 𝐴 ∈ ℂ
5	2	nncni	⊢ 𝐵 ∈ ℂ
6	3	nncni	⊢ 𝐶 ∈ ℂ
7	4 5 6	mulassi	⊢ ( ( 𝐴 · 𝐵 ) · 𝐶 ) = ( 𝐴 · ( 𝐵 · 𝐶 ) )