Metamath Proof Explorer

Theorem ltstrd

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

Proof

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