Metamath Proof Explorer
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 |
|- ( ph -> A < |
|
|
sltssepcd.2 |
|- ( ph -> X e. A ) |
|
|
sltssepcd.3 |
|- ( ph -> Y e. B ) |
|
Assertion |
sltssepcd |
|- ( ph -> X |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
sltssepcd.1 |
|- ( ph -> A < |
| 2 |
|
sltssepcd.2 |
|- ( ph -> X e. A ) |
| 3 |
|
sltssepcd.3 |
|- ( ph -> Y e. B ) |
| 4 |
|
sltssepc |
|- ( ( A < X |
| 5 |
1 2 3 4
|
syl3anc |
|- ( ph -> X |