Theorem sltletr

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

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

Proof

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