# Metamath Proof Explorer

## Theorem eliooord

Description: Ordering implied by a member of an open interval of reals. (Contributed by NM, 17-Aug-2008) (Revised by Mario Carneiro, 9-May-2014)

Ref Expression
Assertion eliooord ${⊢}{A}\in \left({B},{C}\right)\to \left({B}<{A}\wedge {A}<{C}\right)$

### Proof

Step Hyp Ref Expression
1 eliooxr ${⊢}{A}\in \left({B},{C}\right)\to \left({B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)$
2 elioo2 ${⊢}\left({B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left({A}\in \left({B},{C}\right)↔\left({A}\in ℝ\wedge {B}<{A}\wedge {A}<{C}\right)\right)$
3 1 2 syl ${⊢}{A}\in \left({B},{C}\right)\to \left({A}\in \left({B},{C}\right)↔\left({A}\in ℝ\wedge {B}<{A}\wedge {A}<{C}\right)\right)$
4 3 ibi ${⊢}{A}\in \left({B},{C}\right)\to \left({A}\in ℝ\wedge {B}<{A}\wedge {A}<{C}\right)$
5 3simpc ${⊢}\left({A}\in ℝ\wedge {B}<{A}\wedge {A}<{C}\right)\to \left({B}<{A}\wedge {A}<{C}\right)$
6 4 5 syl ${⊢}{A}\in \left({B},{C}\right)\to \left({B}<{A}\wedge {A}<{C}\right)$