Metamath Proof Explorer


Theorem addsubsassd

Description: Associative-type law for surreal addition and subtraction. (Contributed by Scott Fenton, 6-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 addsubsassd.1 φ A No
2 addsubsassd.2 φ B No
3 addsubsassd.3 φ C No
4 3 negscld φ + s C No
5 1 2 4 addsassd φ A + s B + s + s C = A + s B + s + s C
6 1 2 addscld φ A + s B No
7 6 3 subsvald φ A + s B - s C = A + s B + s + s C
8 2 3 subsvald φ B - s C = B + s + s C
9 8 oveq2d φ A + s B - s C = A + s B + s + s C
10 5 7 9 3eqtr4d φ A + s B - s C = A + s B - s C