Metamath Proof Explorer


Theorem addassnni

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

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

Proof

Step Hyp Ref Expression
1 addassnni.1 A
2 addassnni.2 B
3 addassnni.3 C
4 1 nncni A
5 2 nncni B
6 3 nncni C
7 4 5 6 addassi A + B + C = A + B + C