Theorem lestrd

Description: Surreal less-than or equal is transitive. (Contributed by Scott Fenton, 8-Dec-2021)

	Ref	Expression
Hypotheses	ltstrd.1	$$⊢\phi \to A\in \mathrm{No}$$
	ltstrd.2	$$⊢\phi \to B\in \mathrm{No}$$
	ltstrd.3	$$⊢\phi \to C\in \mathrm{No}$$
	lestrd.4	$$⊢\phi \to A{\le }_{s}B$$
	lestrd.5	$$⊢\phi \to B{\le }_{s}C$$
Assertion	lestrd	$$⊢\phi \to A{\le }_{s}C$$

Proof

Step	Hyp	Ref	Expression
1		ltstrd.1	$$⊢\phi \to A\in \mathrm{No}$$
2		ltstrd.2	$$⊢\phi \to B\in \mathrm{No}$$
3		ltstrd.3	$$⊢\phi \to C\in \mathrm{No}$$
4		lestrd.4	$$⊢\phi \to A{\le }_{s}B$$
5		lestrd.5	$$⊢\phi \to B{\le }_{s}C$$
6		lestr	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to \left(\left(A{\le }_{s}B\wedge B{\le }_{s}C\right)\to A{\le }_{s}C\right)$$
7	1 2 3 6	syl3anc	$$⊢\phi \to \left(\left(A{\le }_{s}B\wedge B{\le }_{s}C\right)\to A{\le }_{s}C\right)$$
8	4 5 7	mp2and	$$⊢\phi \to A{\le }_{s}C$$