Theorem slttr

Description: Surreal less than is transitive. (Contributed by Scott Fenton, 16-Jun-2011)

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

Proof

Step	Hyp	Ref	Expression
1		sltso	|-
2		sotr	|- ( ( ( ( A A
3	1 2	mpan	|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A A