Metamath Proof Explorer

Theorem ltsubs1d

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

Ref Expression
Hypotheses ltsubsd.1 ⊢ φ → A ∈ No
ltsubsd.2 ⊢ φ → B ∈ No
ltsubsd.3 ⊢ φ → C ∈ No
Assertion ltsubs1d ⊢ φ → A < s B ↔ A - s C < s B - s C

Proof

Step Hyp Ref Expression
1 ltsubsd.1 ⊢ φ → A ∈ No
2 ltsubsd.2 ⊢ φ → B ∈ No
3 ltsubsd.3 ⊢ φ → C ∈ No
4 ltsubs1 ⊢ 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