Theorem mulassnni

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

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

Proof

Step	Hyp	Ref	Expression
1		mulassnni.1	$$⊢A\in \mathbb{N}$$
2		mulassnni.2	$$⊢B\in \mathbb{N}$$
3		mulassnni.3	$$⊢C\in \mathbb{N}$$
4	1	nncni	$$⊢A\in ℂ$$
5	2	nncni	$$⊢B\in ℂ$$
6	3	nncni	$$⊢C\in ℂ$$
7	4 5 6	mulassi	$$⊢ABC=ABC$$