Metamath Proof Explorer


Theorem adds4d

Description: Rearrangement of four terms in a surreal sum. (Contributed by Scott Fenton, 5-Feb-2025)

Ref Expression
Hypotheses adds4d.1 φ A No
adds4d.2 φ B No
adds4d.3 φ C No
adds4d.4 φ D No
Assertion adds4d φ A + s B + s C + s D = A + s C + s B + s D

Proof

Step Hyp Ref Expression
1 adds4d.1 φ A No
2 adds4d.2 φ B No
3 adds4d.3 φ C No
4 adds4d.4 φ D No
5 1 2 3 adds32d φ A + s B + s C = A + s C + s B
6 5 oveq1d φ A + s B + s C + s D = A + s C + s B + s D
7 1 2 addscld φ A + s B No
8 7 3 4 addsassd φ A + s B + s C + s D = A + s B + s C + s D
9 1 3 addscld φ A + s C No
10 9 2 4 addsassd φ A + s C + s B + s D = A + s C + s B + s D
11 6 8 10 3eqtr3d φ A + s B + s C + s D = A + s C + s B + s D