Metamath Proof Explorer


Theorem mulassnni

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

Ref Expression
Hypotheses mulassnni.1 A
mulassnni.2 B
mulassnni.3 C
Assertion mulassnni A B C = A B C

Proof

Step Hyp Ref Expression
1 mulassnni.1 A
2 mulassnni.2 B
3 mulassnni.3 C
4 1 nncni A
5 2 nncni B
6 3 nncni C
7 4 5 6 mulassi A B C = A B C