Metamath Proof Explorer


Theorem addscan1d

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

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

Proof

Step Hyp Ref Expression
1 addscand.1 φ A No
2 addscand.2 φ B No
3 addscand.3 φ C No
4 addscan1 A No B No C No C + s A = C + s B A = B
5 1 2 3 4 syl3anc φ C + s A = C + s B A = B