Metamath Proof Explorer


Theorem ioogtlb

Description: An element of a closed interval is greater than its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion ioogtlb A*B*CABA<C

Proof

Step Hyp Ref Expression
1 elioo2 A*B*CABCA<CC<B
2 simp2 CA<CC<BA<C
3 1 2 syl6bi A*B*CABA<C
4 3 3impia A*B*CABA<C