Metamath Proof Explorer


Theorem elicod

Description: Membership in a left-closed right-open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses elicod.a φA*
elicod.b φB*
elicod.3 φC*
elicod.4 φAC
elicod.5 φC<B
Assertion elicod φCAB

Proof

Step Hyp Ref Expression
1 elicod.a φA*
2 elicod.b φB*
3 elicod.3 φC*
4 elicod.4 φAC
5 elicod.5 φC<B
6 elico1 A*B*CABC*ACC<B
7 1 2 6 syl2anc φCABC*ACC<B
8 3 4 5 7 mpbir3and φCAB