Metamath Proof Explorer

Theorem elioo5

Description: Membership in an open interval of extended reals. (Contributed by NM, 17-Aug-2008)

Ref Expression
Assertion elioo5 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → C ∈ A B ↔ A < C ∧ C < B

Proof

Step Hyp Ref Expression
1 elioo1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → C ∈ A B ↔ C ∈ ℝ * ∧ A < C ∧ C < B
2 1 3adant3 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → C ∈ A B ↔ C ∈ ℝ * ∧ A < C ∧ C < B
3 3anass ⊢ C ∈ ℝ * ∧ A < C ∧ C < B ↔ C ∈ ℝ * ∧ A < C ∧ C < B
4 3 baibr ⊢ C ∈ ℝ * → A < C ∧ C < B ↔ C ∈ ℝ * ∧ A < C ∧ C < B
5 4 3ad2ant3 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → A < C ∧ C < B ↔ C ∈ ℝ * ∧ A < C ∧ C < B
6 2 5 bitr4d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → C ∈ A B ↔ A < C ∧ C < B