Theorem ssltsepcd

Description: Two elements of separated sets obey less-than. Deduction form of ssltsepc . (Contributed by Scott Fenton, 25-Sep-2024)

	Ref	Expression
Hypotheses	ssltsepcd.1	$$⊢\phi \to A{\ll }_{s}B$$
	ssltsepcd.2	$$⊢\phi \to X\in A$$
	ssltsepcd.3	$$⊢\phi \to Y\in B$$
Assertion	ssltsepcd	$$⊢\phi \to X{<}_{s}Y$$

Proof

Step	Hyp	Ref	Expression
1		ssltsepcd.1	$$⊢\phi \to A{\ll }_{s}B$$
2		ssltsepcd.2	$$⊢\phi \to X\in A$$
3		ssltsepcd.3	$$⊢\phi \to Y\in B$$
4		ssltsepc	$$⊢\left(A{\ll }_{s}B\wedge X\in A\wedge Y\in B\right)\to X{<}_{s}Y$$
5	1 2 3 4	syl3anc	$$⊢\phi \to X{<}_{s}Y$$