Metamath Proof Explorer

Theorem ltlestrd

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
ltlestrd.4 ⊢ φ → A < s B
ltlestrd.5 ⊢ φ → B ≤ s C
Assertion ltlestrd ⊢ φ → A < s C

Proof

Step Hyp Ref Expression
1 ltstrd.1 ⊢ φ → A ∈ No
2 ltstrd.2 ⊢ φ → B ∈ No
3 ltstrd.3 ⊢ φ → C ∈ No
4 ltlestrd.4 ⊢ φ → A < s B
5 ltlestrd.5 ⊢ φ → B ≤ s C
6 ltlestr ⊢ 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