Metamath Proof Explorer


Theorem adds42d

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 adds42d φ A + s B + s C + s D = A + s C + s D + s B

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 4 adds4d φ A + s B + s C + s D = A + s C + s B + s D
6 2 4 addscomd φ B + s D = D + s B
7 6 oveq2d φ A + s C + s B + s D = A + s C + s D + s B
8 5 7 eqtrd φ A + s B + s C + s D = A + s C + s D + s B