Theorem iccleub 13214

Description: An element of a closed interval is less than or equal to its upper bound. (Contributed by Jeff Hankins, 14-Jul-2009.)

Assertion

Ref	Expression
iccleub	⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐶 ≤ 𝐵)

Proof of Theorem iccleub

Step	Hyp	Ref	Expression
1		elicc1 13203	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
2		simp3 1137	. . 3 ⊢ ((𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵) → 𝐶 ≤ 𝐵)
3	1, 2	syl6bi 252	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) → 𝐶 ≤ 𝐵))
4	3	3impia 1116	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐶 ≤ 𝐵)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086   ∈ wcel 2105   class class class wbr 5087  (class class class)co 7317  ℝ^*cxr 11088   ≤ cle 11090  [,]cicc 13162

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pr 5367  ax-un 7630  ax-cnex 11007  ax-resscn 11008

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-sbc 3727  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-br 5088  df-opab 5150  df-id 5507  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-iota 6418  df-fun 6468  df-fv 6474  df-ov 7320  df-oprab 7321  df-mpo 7322  df-xr 11093  df-icc 13166

This theorem is referenced by:  supicc  13313  supiccub  13314  supicclub  13315  oprpiece1res1  24197  ivthlem1  24698  isosctrlem1  26051  ttgcontlem1  27388  broucube  35883  mblfinlem1  35886  ftc1cnnclem  35920  ftc2nc  35931  areaquad  41264  isosctrlem1ALT  42788  lefldiveq  43080  eliccelioc  43309  iccintsng  43311  eliccnelico  43317  eliccelicod  43318  inficc  43322  iccdificc  43327  iccleubd  43336  cncfiooiccre  43686  itgioocnicc  43768  itgspltprt  43770  itgiccshift  43771  fourierdlem1  43899  fourierdlem20  43918  fourierdlem24  43922  fourierdlem25  43923  fourierdlem27  43925  fourierdlem43  43941  fourierdlem44  43942  fourierdlem50  43947  fourierdlem51  43948  fourierdlem52  43949  fourierdlem64  43961  fourierdlem73  43970  fourierdlem76  43973  fourierdlem79  43976  fourierdlem81  43978  fourierdlem92  43989  fourierdlem102  43999  fourierdlem103  44000  fourierdlem104  44001  fourierdlem114  44011  rrxsnicc  44091  salgencntex  44132  sge0p1  44203  hoidmv1lelem3  44382  hoidmvlelem1  44384  hoidmvlelem4  44387