Description: If the upper bound of one closed interval is less than the lower bound of the other, the intervals are disjoint. (Contributed by Zhi Wang, 9-Sep-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | iccdisj |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simplll | ||
2 | simplrr | ||
3 | simpr | ||
4 | iccdisj2 | ||
5 | 1 2 3 4 | syl3anc |