Metamath Proof Explorer


Theorem addassnni

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

Ref Expression
Hypotheses addassnni.1
|- A e. NN
addassnni.2
|- B e. NN
addassnni.3
|- C e. NN
Assertion addassnni
|- ( ( A + B ) + C ) = ( A + ( B + C ) )

Proof

Step Hyp Ref Expression
1 addassnni.1
 |-  A e. NN
2 addassnni.2
 |-  B e. NN
3 addassnni.3
 |-  C e. NN
4 1 nncni
 |-  A e. CC
5 2 nncni
 |-  B e. CC
6 3 nncni
 |-  C e. CC
7 4 5 6 addassi
 |-  ( ( A + B ) + C ) = ( A + ( B + C ) )