Metamath Proof Explorer


Theorem adds32d

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

Ref Expression
Hypotheses addsassd.1 φ A No
addsassd.2 φ B No
addsassd.3 φ C No
Assertion adds32d φ A + s B + s C = A + s C + s B

Proof

Step Hyp Ref Expression
1 addsassd.1 φ A No
2 addsassd.2 φ B No
3 addsassd.3 φ C No
4 2 3 addscomd φ B + s C = C + s B
5 4 oveq2d φ A + s B + s C = A + s C + s B
6 1 2 3 addsassd φ A + s B + s C = A + s B + s C
7 1 3 2 addsassd φ A + s C + s B = A + s C + s B
8 5 6 7 3eqtr4d φ A + s B + s C = A + s C + s B