Metamath Proof Explorer

Theorem elicc4

Description: Membership in a closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014) (Proof shortened by Mario Carneiro, 1-Jan-2017)

Ref Expression
Assertion elicc4 
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( C e. ( A [,] B ) <-> ( A <_ C /\ C <_ B ) ) )

Proof

Step Hyp Ref Expression
1 elicc1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A [,] B ) <-> ( C e. RR* /\ A <_ C /\ C <_ B ) ) )
2 3anass 
 |-  ( ( C e. RR* /\ A <_ C /\ C <_ B ) <-> ( C e. RR* /\ ( A <_ C /\ C <_ B ) ) )
3 1 2 bitrdi 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A [,] B ) <-> ( C e. RR* /\ ( A <_ C /\ C <_ B ) ) ) )
4 3 baibd 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) -> ( C e. ( A [,] B ) <-> ( A <_ C /\ C <_ B ) ) )
5 4 3impa 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( C e. ( A [,] B ) <-> ( A <_ C /\ C <_ B ) ) )