Metamath Proof Explorer


Theorem nncansd

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

Ref Expression
Hypotheses nncansd.1 φ A No
nncansd.2 φ B No
Assertion nncansd φ A - s A - s B = B

Proof

Step Hyp Ref Expression
1 nncansd.1 φ A No
2 nncansd.2 φ B No
3 1 1 2 subsubs2d φ A - s A - s B = A + s B - s A
4 pncan3s A No B No A + s B - s A = B
5 1 2 4 syl2anc φ A + s B - s A = B
6 3 5 eqtrd φ A - s A - s B = B