Theorem iccleub 13348

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 13336	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
2		simp3 1139	. . 3 ⊢ ((𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵) → 𝐶 ≤ 𝐵)
3	1, 2	biimtrdi 253	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) → 𝐶 ≤ 𝐵))
4	3	3impia 1118	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐶 ≤ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2114   class class class wbr 5086  (class class class)co 7361  ℝ^*cxr 11172   ≤ cle 11174  [,]cicc 13295

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 2185  ax-ext 2709  ax-sep 5232  ax-pr 5371  ax-un 7683  ax-cnex 11088  ax-resscn 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6449  df-fun 6495  df-fv 6501  df-ov 7364  df-oprab 7365  df-mpo 7366  df-xr 11177  df-icc 13299

This theorem is referenced by:  supicc  13448  supiccub  13449  supicclub  13450  oprpiece1res1  24931  ivthlem1  25431  isosctrlem1  26798  ttgcontlem1  28970  broucube  37992  mblfinlem1  37995  ftc1cnnclem  38029  ftc2nc  38040  areaquad  43665  isosctrlem1ALT  45381  lefldiveq  45746  eliccelioc  45972  iccintsng  45974  eliccnelico  45980  eliccelicod  45981  inficc  45985  iccdificc  45990  iccleubd  45999  cncfiooiccre  46344  itgioocnicc  46426  itgspltprt  46428  itgiccshift  46429  fourierdlem1  46557  fourierdlem20  46576  fourierdlem24  46580  fourierdlem25  46581  fourierdlem27  46583  fourierdlem43  46599  fourierdlem44  46600  fourierdlem50  46605  fourierdlem51  46606  fourierdlem52  46607  fourierdlem64  46619  fourierdlem73  46628  fourierdlem76  46631  fourierdlem79  46634  fourierdlem81  46636  fourierdlem92  46647  fourierdlem102  46657  fourierdlem103  46658  fourierdlem104  46659  fourierdlem114  46669  rrxsnicc  46749  salgencntex  46792  sge0p1  46863  hoidmv1lelem3  47042  hoidmvlelem1  47044  hoidmvlelem4  47047