Metamath Proof Explorer

Theorem ltstr

Description: Surreal less-than is transitive. (Contributed by Scott Fenton, 16-Jun-2011)

Ref Expression
Assertion ltstr ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A < s B ∧ B < s C → A < s C

Proof

Step Hyp Ref Expression
1 ltsso ⊢ < s Or No
2 sotr ⊢ < s Or No ∧ A ∈ No ∧ B ∈ No ∧ C ∈ No → A < s B ∧ B < s C → A < s C
3 1 2 mpan ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A < s B ∧ B < s C → A < s C