Theorem sltssepcd

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

	Ref	Expression
Hypotheses	sltssepcd.1	⊢ ( 𝜑 → 𝐴 <<s 𝐵 )
	sltssepcd.2	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	sltssepcd.3	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	sltssepcd	⊢ ( 𝜑 → 𝑋 <s 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		sltssepcd.1	⊢ ( 𝜑 → 𝐴 <<s 𝐵 )
2		sltssepcd.2	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
3		sltssepcd.3	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
4		sltssepc	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 <s 𝑌 )
5	1 2 3 4	syl3anc	⊢ ( 𝜑 → 𝑋 <s 𝑌 )