Theorem sletr

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

	Ref	Expression
Assertion	sletr	|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A <_s B /\ B <_s C ) -> A <_s C ) )

Proof

Step	Hyp	Ref	Expression
1		sltletr	|- ( ( C e. No /\ A e. No /\ B e. No ) -> ( ( C C
2	1	3coml	|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( C C
3	2	expcomd	|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( A <_s B -> ( C C
4	3	imp	|- ( ( ( A e. No /\ B e. No /\ C e. No ) /\ A <_s B ) -> ( C C
5	4	con3d	|- ( ( ( A e. No /\ B e. No /\ C e. No ) /\ A <_s B ) -> ( -. C -. C
6	5	expimpd	|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A <_s B /\ -. C -. C
7		slenlt	|- ( ( B e. No /\ C e. No ) -> ( B <_s C <-> -. C
8	7	3adant1	|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( B <_s C <-> -. C
9	8	anbi2d	|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A <_s B /\ B <_s C ) <-> ( A <_s B /\ -. C
10		slenlt	|- ( ( A e. No /\ C e. No ) -> ( A <_s C <-> -. C
11	10	3adant2	|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( A <_s C <-> -. C
12	6 9 11	3imtr4d	|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A <_s B /\ B <_s C ) -> A <_s C ) )