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*B*C*CABA<CC<B

Proof

Step Hyp Ref Expression
1 elioo1 A*B*CABC*A<CC<B
2 1 3adant3 A*B*C*CABC*A<CC<B
3 3anass C*A<CC<BC*A<CC<B
4 3 baibr C*A<CC<BC*A<CC<B
5 4 3ad2ant3 A*B*C*A<CC<BC*A<CC<B
6 2 5 bitr4d A*B*C*CABA<CC<B