Theorem eliooord 12615

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 12614	. . . 4 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*))
2		elioo2 12598	. . . 4 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 ∈ (𝐵(,)𝐶) ↔ (𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶)))
3	1, 2	syl 17	. . 3 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐴 ∈ (𝐵(,)𝐶) ↔ (𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶)))
4	3	ibi 259	. 2 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶))
5		3simpc 1130	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶) → (𝐵 < 𝐴 ∧ 𝐴 < 𝐶))
6	4, 5	syl 17	1 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 < 𝐴 ∧ 𝐴 < 𝐶))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   ∧ w3a 1068   ∈ wcel 2050   class class class wbr 4930  (class class class)co 6978  ℝcr 10336  ℝ^*cxr 10475   < clt 10476  (,)cioo 12557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pow 5120  ax-pr 5187  ax-un 7281  ax-cnex 10393  ax-resscn 10394  ax-pre-lttri 10411  ax-pre-lttrn 10412

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4181  df-if 4352  df-pw 4425  df-sn 4443  df-pr 4445  df-op 4449  df-uni 4714  df-iun 4795  df-br 4931  df-opab 4993  df-mpt 5010  df-id 5313  df-po 5327  df-so 5328  df-xp 5414  df-rel 5415  df-cnv 5416  df-co 5417  df-dm 5418  df-rn 5419  df-res 5420  df-ima 5421  df-iota 6154  df-fun 6192  df-fn 6193  df-f 6194  df-f1 6195  df-fo 6196  df-f1o 6197  df-fv 6198  df-ov 6981  df-oprab 6982  df-mpo 6983  df-1st 7503  df-2nd 7504  df-er 8091  df-en 8309  df-dom 8310  df-sdom 8311  df-pnf 10478  df-mnf 10479  df-xr 10480  df-ltxr 10481  df-le 10482  df-ioo 12561

This theorem is referenced by:  elioo4g  12616  iccssioo2  12628  qdensere  23084  zcld  23127  reconnlem2  23141  xrge0tsms  23148  ovolioo  23875  ioorcl2  23879  itgsplitioo  24144  dvferm1lem  24287  dvferm2lem  24289  dvferm  24291  dvlt0  24308  dvivthlem1  24311  lhop1lem  24316  lhop1  24317  lhop2  24318  dvcvx  24323  ftc1lem4  24342  itgsubstlem  24351  itgsubst  24352  pilem2  24746  pilem3  24747  pigt2lt4  24748  tangtx  24797  tanabsge  24798  cosne0  24818  tanord  24826  tanregt0  24827  argimlt0  24900  logneg2  24902  divlogrlim  24922  logno1  24923  logcnlem3  24931  dvloglem  24935  logf1o2  24937  loglesqrt  25043  asinsin  25174  acoscos  25175  atanlogaddlem  25195  atanlogsub  25198  atantan  25205  atanbndlem  25207  scvxcvx  25268  lgamgulmlem2  25312  basellem8  25370  vmalogdivsum2  25819  vmalogdivsum  25820  2vmadivsumlem  25821  chpdifbndlem1  25834  selberg3lem1  25838  selberg3  25840  selberg4lem1  25841  selberg4  25842  selberg3r  25850  selberg4r  25851  selberg34r  25852  pntrlog2bndlem1  25858  pntrlog2bndlem2  25859  pntrlog2bndlem3  25860  pntrlog2bndlem4  25861  pntrlog2bndlem5  25862  pntrlog2bndlem6a  25863  pntrlog2bndlem6  25864  pntrlog2bnd  25865  pntpbnd1a  25866  pntpbnd1  25867  pntpbnd2  25868  pntpbnd  25869  pntibndlem2  25872  pntibndlem3  25873  pntibnd  25874  pntlemd  25875  pntlemb  25878  pntlemr  25883  pnt  25895  padicabv  25911  xrge0tsmsd  30530  fct2relem  31516  logdivsqrle  31569  knoppndvlem3  33373  iooelexlt  34085  relowlssretop  34086  poimir  34366  itg2gt0cn  34388  ftc1cnnclem  34406  radcnvrat  40062  cncfiooicclem1  41607  itgioocnicc  41693  iblcncfioo  41694  amgmwlem  44271