Metamath Proof Explorer

Theorem sltletrd

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

Proof

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