Metamath Proof Explorer


Theorem sltsub1d

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 sltsub1d φ A < s B A - s C < s B - s C

Proof

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