Metamath Proof Explorer


Theorem sltadd2d

Description: Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025)

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

Proof

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