Theorem eliocd

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

	Ref	Expression
Hypotheses	eliocd.a	$$⊢\phi \to A\in {ℝ}^{*}$$
	eliocd.b	$$⊢\phi \to B\in {ℝ}^{*}$$
	eliocd.c	$$⊢\phi \to C\in {ℝ}^{*}$$
	eliocd.altc	$$⊢\phi \to A<C$$
	eliocd.cleb	$$⊢\phi \to C\le B$$
Assertion	eliocd	$$⊢\phi \to C\in \left(A,B\right]$$

Proof

Step	Hyp	Ref	Expression
1		eliocd.a	$$⊢\phi \to A\in {ℝ}^{*}$$
2		eliocd.b	$$⊢\phi \to B\in {ℝ}^{*}$$
3		eliocd.c	$$⊢\phi \to C\in {ℝ}^{*}$$
4		eliocd.altc	$$⊢\phi \to A<C$$
5		eliocd.cleb	$$⊢\phi \to C\le B$$
6		elioc1	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(C\in \left(A,B\right]\leftrightarrow \left(C\in {ℝ}^{*}\wedge A<C\wedge C\le B\right)\right)$$
7	1 2 6	syl2anc	$$⊢\phi \to \left(C\in \left(A,B\right]\leftrightarrow \left(C\in {ℝ}^{*}\wedge A<C\wedge C\le B\right)\right)$$
8	3 4 5 7	mpbir3and	$$⊢\phi \to C\in \left(A,B\right]$$