Metamath Proof Explorer


Theorem adds12d

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

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

Proof

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