Metamath Proof Explorer


Theorem subsubs2d

Description: Law for double surreal subtraction. (Contributed by Scott Fenton, 16-Apr-2025)

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

Proof

Step Hyp Ref Expression
1 subsubs4d.1 φ A No
2 subsubs4d.2 φ B No
3 subsubs4d.3 φ C No
4 2 3 subscld φ B - s C No
5 1 4 subsvald φ A - s B - s C = A + s + s B - s C
6 2 3 negsubsdi2d φ + s B - s C = C - s B
7 6 oveq2d φ A + s + s B - s C = A + s C - s B
8 5 7 eqtrd φ A - s B - s C = A + s C - s B