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