Metamath Proof Explorer


Theorem sltsub2d

Description: Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 5-Feb-2025)

Ref Expression
Hypotheses sltsubd.1 φ A No
sltsubd.2 φ B No
sltsubd.3 φ C No
Assertion sltsub2d φ A < s B C - s B < s C - s A

Proof

Step Hyp Ref Expression
1 sltsubd.1 φ A No
2 sltsubd.2 φ B No
3 sltsubd.3 φ C No
4 sltsub2 A No B No C No A < s B C - s B < s C - s A
5 1 2 3 4 syl3anc φ A < s B C - s B < s C - s A