Metamath Proof Explorer


Theorem pncan2s

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

Ref Expression
Assertion pncan2s A No B No A + s B - s A = B

Proof

Step Hyp Ref Expression
1 eqid A + s B = A + s B
2 addscl A No B No A + s B No
3 simpl A No B No A No
4 simpr A No B No B No
5 2 3 4 subaddsd A No B No A + s B - s A = B A + s B = A + s B
6 1 5 mpbiri A No B No A + s B - s A = B