Theorem slelttr

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

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

Proof

Step	Hyp	Ref	Expression
1		slenlt	|- ( ( A e. No /\ B e. No ) -> ( A <_s B <-> -. B
2	1	3adant3	|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( A <_s B <-> -. B
3	2	anbi1d	|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A <_s B /\ B ( -. B
4		sltso	|-
5		sotr2	|- ( ( ( ( -. B A
6	4 5	mpan	|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( -. B A
7	3 6	sylbid	|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A <_s B /\ B A