Metamath Proof Explorer

Theorem slttrd

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

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

Proof

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