Theorem slttrd

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