Metamath Proof Explorer


Theorem addscan2d

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 addscan2d φ A + s C = B + s C A = B

Proof

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