Theorem eliood 46331

Description: Membership in an open real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
eliood.1	⊢ (𝜑 → 𝐴 ∈ ℝ*)
eliood.2	⊢ (𝜑 → 𝐵 ∈ ℝ*)
eliood.3	⊢ (𝜑 → 𝐶 ∈ ℝ)
eliood.4	⊢ (𝜑 → 𝐴 < 𝐶)
eliood.5	⊢ (𝜑 → 𝐶 < 𝐵)

Assertion

Ref	Expression
eliood	⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))

Proof of Theorem eliood

Step	Hyp	Ref	Expression
1		eliood.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℝ)
2		eliood.4	. 2 ⊢ (𝜑 → 𝐴 < 𝐶)
3		eliood.5	. 2 ⊢ (𝜑 → 𝐶 < 𝐵)
4		eliood.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
5		eliood.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
6		elioo2 13442	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
7	4, 5, 6	syl2anc 596	. 2 ⊢ (𝜑 → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
8	1, 2, 3, 7	mpbir3and 1361	1 ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103   ∈ wcel 2145   class class class wbr 5103  (class class class)co 7414  ℝcr 11126  ℝ^*cxr 11269   < clt 11270  (,)cioo 13401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-cnex 11183  ax-resscn 11184  ax-pre-lttri 11201  ax-pre-lttrn 11202

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7417  df-oprab 7418  df-mpo 7419  df-1st 7987  df-2nd 7988  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-ioo 13405

This theorem is used by:  ioomidp  46347  iocopn  46353  iooshift  46355  icoopn  46358  qinioo  46368  qelioo  46379  icomnfinre  46385  ressioosup  46388  ressiooinf  46390  uzubioo  46398  limciccioolb  46454  limcicciooub  46468  lptre2pt  46471  limcresiooub  46473  limcresioolb  46474  limcleqr  46475  xlimxrre  46662  cncfiooiccre  46726  dvbdfbdioolem2  46760  dvbdfbdioo  46761  ioodvbdlimc1lem1  46762  ioodvbdlimc1lem2  46763  ioodvbdlimc2lem  46765  itgioocnicc  46808  dirkercncflem1  46934  dirkercncflem4  46937  fourierdlem10  46948  fourierdlem20  46958  fourierdlem25  46963  fourierdlem27  46965  fourierdlem28  46966  fourierdlem31  46969  fourierdlem32  46970  fourierdlem33  46971  fourierdlem40  46978  fourierdlem41  46979  fourierdlem43  46981  fourierdlem44  46982  fourierdlem46  46983  fourierdlem48  46985  fourierdlem49  46986  fourierdlem57  46994  fourierdlem59  46996  fourierdlem60  46997  fourierdlem61  46998  fourierdlem62  46999  fourierdlem64  47001  fourierdlem68  47005  fourierdlem73  47010  fourierdlem74  47011  fourierdlem75  47012  fourierdlem76  47013  fourierdlem78  47015  fourierdlem81  47018  fourierdlem82  47019  fourierdlem84  47021  fourierdlem89  47026  fourierdlem90  47027  fourierdlem91  47028  fourierdlem92  47029  fourierdlem93  47030  fourierdlem97  47034  fourierdlem103  47040  fourierdlem104  47041  fourierdlem107  47044  fourierdlem109  47046  fourierdlem111  47048  fourierdlem112  47049  sqwvfourb  47060  fourierswlem  47061  fouriersw  47062  qndenserrnbllem  47125  ioorrnopnlem  47135  ioorrnopnxrlem  47137  hspdifhsp  47447  hspmbllem2  47458  pimiooltgt  47541  pimrecltneg  47555  smfresal  47619  smfmullem2  47623