Metamath Proof Explorer

Theorem sltadd1d

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

Ref Expression
Hypotheses addscand.1 ⊢ φ → A ∈ No
addscand.2 ⊢ φ → B ∈ No
addscand.3 ⊢ φ → C ∈ No
Assertion sltadd1d ⊢ φ → A < s B ↔ A + s C < s B + s C

Proof

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