Metamath Proof Explorer


Theorem subaddsd

Description: Relationship between addition and subtraction for surreals. (Contributed by Scott Fenton, 5-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 subaddsd.1 φ A No
2 subaddsd.2 φ B No
3 subaddsd.3 φ C No
4 subadds A No B No C No A - s B = C B + s C = A
5 1 2 3 4 syl3anc φ A - s B = C B + s C = A