Metamath Proof Explorer

Theorem slttr

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

		Ref	Expression
	Assertion	slttr	$⊢ (A \in No \land B \in No \land C \in No) \to ((A <_{s} B \land B <_{s} C) \to A <_{s} C)$

Step	Hyp	Ref	Expression
1		sltso	$⊢ <_{s} Or No$
2		sotr	$⊢ (<_{s} Or No \land (A \in No \land B \in No \land C \in No)) \to ((A <_{s} B \land B <_{s} C) \to A <_{s} C)$
3	1 2	mpan	$⊢ (A \in No \land B \in No \land C \in No) \to ((A <_{s} B \land B <_{s} C) \to A <_{s} C)$