Theorem sletrd

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

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

Proof

Step	Hyp	Ref	Expression
1		slttrd.1	$$⊢\phi \to A\in \mathrm{No}$$
2		slttrd.2	$$⊢\phi \to B\in \mathrm{No}$$
3		slttrd.3	$$⊢\phi \to C\in \mathrm{No}$$
4		sletrd.4	$$⊢\phi \to A{\le }_{s}B$$
5		sletrd.5	$$⊢\phi \to B{\le }_{s}C$$
6		sletr	$$⊢\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$$