Theorem iccleub 12433

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 12423	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
2		simp3 1131	. . 3 ⊢ ((𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵) → 𝐶 ≤ 𝐵)
3	1, 2	syl6bi 243	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) → 𝐶 ≤ 𝐵))
4	3	3impia 1108	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐶 ≤ 𝐵)

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1070   ∈ wcel 2144   class class class wbr 4784  (class class class)co 6792  ℝ^*cxr 10274   ≤ cle 10276  [,]cicc 12382

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pr 5034  ax-un 7095  ax-cnex 10193  ax-resscn 10194

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-sbc 3586  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-br 4785  df-opab 4845  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-iota 5994  df-fun 6033  df-fv 6039  df-ov 6795  df-oprab 6796  df-mpt2 6797  df-xr 10279  df-icc 12386

This theorem is referenced by:  supicc  12526  supiccub  12527  supicclub  12528  oprpiece1res1  22969  ivthlem1  23438  isosctrlem1  24768  ttgcontlem1  25985  broucube  33769  mblfinlem1  33772  ftc1cnnclem  33808  ftc2nc  33819  areaquad  38321  isosctrlem1ALT  39686  lefldiveq  40017  eliccelioc  40260  iccintsng  40262  eliccnelico  40268  eliccelicod  40269  inficc  40273  iccdificc  40278  iccleubd  40287  cncfiooiccre  40620  itgioocnicc  40704  itgspltprt  40706  itgiccshift  40707  fourierdlem1  40836  fourierdlem20  40855  fourierdlem24  40859  fourierdlem25  40860  fourierdlem27  40862  fourierdlem43  40878  fourierdlem44  40879  fourierdlem50  40884  fourierdlem51  40885  fourierdlem52  40886  fourierdlem64  40898  fourierdlem73  40907  fourierdlem76  40910  fourierdlem79  40913  fourierdlem81  40915  fourierdlem92  40926  fourierdlem102  40936  fourierdlem103  40937  fourierdlem104  40938  fourierdlem114  40948  rrxsnicc  41031  salgencntex  41072  sge0p1  41142  hoidmv1lelem3  41321  hoidmvlelem1  41323  hoidmvlelem4  41326