This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iocgtlbd

Description: An element of a left-open right-closed interval is larger than its lower bound. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses iocgtlbd.1 ⊢ φ → A ∈ ℝ *
iocgtlbd.2 ⊢ φ → B ∈ ℝ *
iocgtlbd.3 ⊢ φ → C ∈ A B
Assertion iocgtlbd ⊢ φ → A < C

Proof

Step Hyp Ref Expression
1 iocgtlbd.1 ⊢ φ → A ∈ ℝ *
2 iocgtlbd.2 ⊢ φ → B ∈ ℝ *
3 iocgtlbd.3 ⊢ φ → C ∈ A B
4 iocgtlb ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ A B → A < C
5 1 2 3 4 syl3anc ⊢ φ → A < C