Metamath Proof Explorer


Theorem nadd32

Description: Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by Scott Fenton, 20-Jan-2025)

Ref Expression
Assertion nadd32 A On B On C On A + B + C = A + C + B

Proof

Step Hyp Ref Expression
1 naddcom B On C On B + C = C + B
2 1 3adant1 A On B On C On B + C = C + B
3 2 oveq2d A On B On C On A + B + C = A + C + B
4 naddass A On B On C On A + B + C = A + B + C
5 naddass A On C On B On A + C + B = A + C + B
6 5 3com23 A On B On C On A + C + B = A + C + B
7 3 4 6 3eqtr4d A On B On C On A + B + C = A + C + B