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 e. RR* /\ B e. RR* /\ C e. RR* ) -> ( C e. ( A (,) B ) <-> ( A < C /\ C < B ) ) )

Proof

Step Hyp Ref Expression
1 elioo1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,) B ) <-> ( C e. RR* /\ A < C /\ C < B ) ) )
2 1 3adant3 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( C e. ( A (,) B ) <-> ( C e. RR* /\ A < C /\ C < B ) ) )
3 3anass 
 |-  ( ( C e. RR* /\ A < C /\ C < B ) <-> ( C e. RR* /\ ( A < C /\ C < B ) ) )
4 3 baibr 
 |-  ( C e. RR* -> ( ( A < C /\ C < B ) <-> ( C e. RR* /\ A < C /\ C < B ) ) )
5 4 3ad2ant3 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A < C /\ C < B ) <-> ( C e. RR* /\ A < C /\ C < B ) ) )
6 2 5 bitr4d 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( C e. ( A (,) B ) <-> ( A < C /\ C < B ) ) )