Metamath Proof Explorer


Theorem sletr

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

Ref Expression
Assertion sletr A No B No C No A s B B s C A s C

Proof

Step Hyp Ref Expression
1 sltletr C No A No B No C < s A A s B C < s B
2 1 3coml A No B No C No C < s A A s B C < s B
3 2 expcomd A No B No C No A s B C < s A C < s B
4 3 imp A No B No C No A s B C < s A C < s B
5 4 con3d A No B No C No A s B ¬ C < s B ¬ C < s A
6 5 expimpd A No B No C No A s B ¬ C < s B ¬ C < s A
7 slenlt B No C No B s C ¬ C < s B
8 7 3adant1 A No B No C No B s C ¬ C < s B
9 8 anbi2d A No B No C No A s B B s C A s B ¬ C < s B
10 slenlt A No C No A s C ¬ C < s A
11 10 3adant2 A No B No C No A s C ¬ C < s A
12 6 9 11 3imtr4d A No B No C No A s B B s C A s C