Metamath Proof Explorer


Theorem slelttr

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

Ref Expression
Assertion slelttr A No B No C No A s B B < s C A < s C

Proof

Step Hyp Ref Expression
1 slenlt A No B No A s B ¬ B < s A
2 1 3adant3 A No B No C No A s B ¬ B < s A
3 2 anbi1d A No B No C No A s B B < s C ¬ B < s A B < s C
4 sltso < s Or No
5 sotr2 < s Or No A No B No C No ¬ B < s A B < s C A < s C
6 4 5 mpan A No B No C No ¬ B < s A B < s C A < s C
7 3 6 sylbid A No B No C No A s B B < s C A < s C