Metamath Proof Explorer


Theorem pncans

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

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

Proof

Step Hyp Ref Expression
1 addscom A No B No A + s B = B + s A
2 1 eqcomd A No B No B + s A = A + s B
3 addscl A No B No A + s B No
4 simpr A No B No B No
5 simpl A No B No A No
6 3 4 5 subaddsd A No B No A + s B - s B = A B + s A = A + s B
7 2 6 mpbird A No B No A + s B - s B = A