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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
iocgtlbd.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
iocgtlbd.3 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 (,] 𝐵 ) )
Assertion iocgtlbd ( 𝜑 → 𝐴 < 𝐶 )

Proof

Step Hyp Ref Expression
1 iocgtlbd.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2 iocgtlbd.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3 iocgtlbd.3 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 (,] 𝐵 ) )
4 iocgtlb ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐴 < 𝐶 )
5 1 2 3 4 syl3anc ⊢ ( 𝜑 → 𝐴 < 𝐶 )