Theorem slelttrd

Description: Surreal less-than 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}$$
	slelttrd.4	$$⊢\phi \to A{\le }_{s}B$$
	slelttrd.5	$$⊢\phi \to B{<}_{s}C$$
Assertion	slelttrd	$$⊢\phi \to A{<}_{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		slelttrd.4	$$⊢\phi \to A{\le }_{s}B$$
5		slelttrd.5	$$⊢\phi \to B{<}_{s}C$$
6		slelttr	$$⊢\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{<}_{s}C\right)\to A{<}_{s}C\right)$$
7	1 2 3 6	syl3anc	$$⊢\phi \to \left(\left(A{\le }_{s}B\wedge B{<}_{s}C\right)\to A{<}_{s}C\right)$$
8	4 5 7	mp2and	$$⊢\phi \to A{<}_{s}C$$