Theorem eliooord 13347

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2114   class class class wbr 5074  (class class class)co 7356  ℝcr 11026  ℝ^*cxr 11167   < clt 11168  (,)cioo 13287

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2184  ax-ext 2707  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7678  ax-cnex 11083  ax-resscn 11084  ax-pre-lttri 11101  ax-pre-lttrn 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-iun 4925  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-po 5528  df-so 5529  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-ov 7359  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932  df-er 8632  df-en 8883  df-dom 8884  df-sdom 8885  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-ioo 13291

This theorem is referenced by:  elioo4g  13348  iccssioo2  13361  qdensere  24722  zcld  24767  reconnlem2  24781  xrge0tsms  24788  ovolioo  25523  ioorcl2  25527  itgsplitioo  25793  dvferm1lem  25939  dvferm2lem  25941  dvferm  25943  dvlt0  25960  dvivthlem1  25963  lhop1lem  25968  lhop1  25969  lhop2  25970  dvcvx  25975  ftc1lem4  25994  itgsubstlem  26003  itgsubst  26004  pilem2  26405  pilem3  26406  pigt2lt4  26407  tangtx  26457  tanabsge  26458  cosne0  26481  cos0pilt1  26484  tanord  26490  tanregt0  26491  argimlt0  26565  logneg2  26567  divlogrlim  26587  logno1  26588  logcnlem3  26596  dvloglem  26600  logf1o2  26602  loglesqrt  26713  asinsin  26844  acoscos  26845  atanlogaddlem  26865  atanlogsub  26868  atantan  26875  atanbndlem  26877  scvxcvx  26937  lgamgulmlem2  26981  basellem8  27039  vmalogdivsum2  27489  vmalogdivsum  27490  2vmadivsumlem  27491  chpdifbndlem1  27504  selberg3lem1  27508  selberg3  27510  selberg4lem1  27511  selberg4  27512  selberg3r  27520  selberg4r  27521  selberg34r  27522  pntrlog2bndlem1  27528  pntrlog2bndlem2  27529  pntrlog2bndlem3  27530  pntrlog2bndlem4  27531  pntrlog2bndlem5  27532  pntrlog2bndlem6a  27533  pntrlog2bndlem6  27534  pntrlog2bnd  27535  pntpbnd1a  27536  pntpbnd1  27537  pntpbnd2  27538  pntpbnd  27539  pntibndlem2  27542  pntibndlem3  27543  pntibnd  27544  pntlemd  27545  pntlemb  27548  pntlemr  27553  pnt  27565  padicabv  27581  xrge0tsmsd  33122  fct2relem  34729  logdivsqrle  34782  knoppndvlem3  36762  iooelexlt  37666  relowlssretop  37667  poimir  37962  itg2gt0cn  37984  ftc1cnnclem  38000  aks4d1p1p5  42502  radcnvrat  44729  cncfiooicclem1  46309  itgioocnicc  46393  iblcncfioo  46394  amgmwlem  50265