Metamath Proof Explorer

Theorem leltstrd

Description: Surreal less-than is transitive. (Contributed by Scott Fenton, 8-Dec-2021)

Ref Expression
Hypotheses ltstrd.1 ⊢ φ → A ∈ No
ltstrd.2 ⊢ φ → B ∈ No
ltstrd.3 ⊢ φ → C ∈ No
leltstrd.4 ⊢ φ → A ≤ s B
leltstrd.5 ⊢ φ → B < s C
Assertion leltstrd ⊢ φ → A < s C

Proof

Step Hyp Ref Expression
1 ltstrd.1 ⊢ φ → A ∈ No
2 ltstrd.2 ⊢ φ → B ∈ No
3 ltstrd.3 ⊢ φ → C ∈ No
4 leltstrd.4 ⊢ φ → A ≤ s B
5 leltstrd.5 ⊢ φ → B < s C
6 leltstr ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A ≤ s B ∧ B < s C → A < s C
7 1 2 3 6 syl3anc ⊢ φ → A ≤ s B ∧ B < s C → A < s C
8 4 5 7 mp2and ⊢ φ → A < s C