Theorem eliooord 13385

Description: Ordering implied by a member of an open interval of reals. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 9-May-2014.)

Assertion

Ref	Expression
eliooord	⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 < 𝐴 ∧ 𝐴 < 𝐶))

Proof of Theorem eliooord

Step	Hyp	Ref	Expression
1		eliooxr 13384	. . . 4 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*))
2		elioo2 13367	. . . 4 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 ∈ (𝐵(,)𝐶) ↔ (𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶)))
3	1, 2	syl 17	. . 3 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐴 ∈ (𝐵(,)𝐶) ↔ (𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶)))
4	3	ibi 266	. 2 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶))
5		3simpc 1150	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶) → (𝐵 < 𝐴 ∧ 𝐴 < 𝐶))
6	4, 5	syl 17	1 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 < 𝐴 ∧ 𝐴 < 𝐶))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   ∈ wcel 2106   class class class wbr 5148  (class class class)co 7411  ℝcr 11111  ℝ^*cxr 11249   < clt 11250  (,)cioo 13326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-pre-lttri 11186  ax-pre-lttrn 11187

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7977  df-2nd 7978  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-ioo 13330

This theorem is referenced by:  elioo4g  13386  iccssioo2  13399  qdensere  24293  zcld  24336  reconnlem2  24350  xrge0tsms  24357  ovolioo  25092  ioorcl2  25096  itgsplitioo  25362  dvferm1lem  25508  dvferm2lem  25510  dvferm  25512  dvlt0  25529  dvivthlem1  25532  lhop1lem  25537  lhop1  25538  lhop2  25539  dvcvx  25544  ftc1lem4  25563  itgsubstlem  25572  itgsubst  25573  pilem2  25971  pilem3  25972  pigt2lt4  25973  tangtx  26022  tanabsge  26023  cosne0  26045  cos0pilt1  26048  tanord  26054  tanregt0  26055  argimlt0  26128  logneg2  26130  divlogrlim  26150  logno1  26151  logcnlem3  26159  dvloglem  26163  logf1o2  26165  loglesqrt  26273  asinsin  26404  acoscos  26405  atanlogaddlem  26425  atanlogsub  26428  atantan  26435  atanbndlem  26437  scvxcvx  26497  lgamgulmlem2  26541  basellem8  26599  vmalogdivsum2  27048  vmalogdivsum  27049  2vmadivsumlem  27050  chpdifbndlem1  27063  selberg3lem1  27067  selberg3  27069  selberg4lem1  27070  selberg4  27071  selberg3r  27079  selberg4r  27080  selberg34r  27081  pntrlog2bndlem1  27087  pntrlog2bndlem2  27088  pntrlog2bndlem3  27089  pntrlog2bndlem4  27090  pntrlog2bndlem5  27091  pntrlog2bndlem6a  27092  pntrlog2bndlem6  27093  pntrlog2bnd  27094  pntpbnd1a  27095  pntpbnd1  27096  pntpbnd2  27097  pntpbnd  27098  pntibndlem2  27101  pntibndlem3  27102  pntibnd  27103  pntlemd  27104  pntlemb  27107  pntlemr  27112  pnt  27124  padicabv  27140  xrge0tsmsd  32250  fct2relem  33678  logdivsqrle  33731  knoppndvlem3  35476  iooelexlt  36329  relowlssretop  36330  poimir  36607  itg2gt0cn  36629  ftc1cnnclem  36645  aks4d1p1p5  41026  radcnvrat  43155  cncfiooicclem1  44688  itgioocnicc  44772  iblcncfioo  44773  amgmwlem  47927