Theorem sltletrd

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}$$
	sltletrd.4	$$⊢\phi \to A{<}_{s}B$$
	sltletrd.5	$$⊢\phi \to B{\le }_{s}C$$
Assertion	sltletrd	$$⊢\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		sltletrd.4	$$⊢\phi \to A{<}_{s}B$$
5		sltletrd.5	$$⊢\phi \to B{\le }_{s}C$$
6		sltletr	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to \left(\left(A{<}_{s}B\wedge B{\le }_{s}C\right)\to A{<}_{s}C\right)$$
7	1 2 3 6	syl3anc	$$⊢\phi \to \left(\left(A{<}_{s}B\wedge B{\le }_{s}C\right)\to A{<}_{s}C\right)$$
8	4 5 7	mp2and	$$⊢\phi \to A{<}_{s}C$$