Theorem iccleub 12642

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1080   ∈ wcel 2081   class class class wbr 4962  (class class class)co 7016  ℝ^*cxr 10520   ≤ cle 10522  [,]cicc 12591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pr 5221  ax-un 7319  ax-cnex 10439  ax-resscn 10440

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-iota 6189  df-fun 6227  df-fv 6233  df-ov 7019  df-oprab 7020  df-mpo 7021  df-xr 10525  df-icc 12595

This theorem is referenced by:  supicc  12736  supiccub  12737  supicclub  12738  oprpiece1res1  23238  ivthlem1  23735  isosctrlem1  25077  ttgcontlem1  26354  broucube  34457  mblfinlem1  34460  ftc1cnnclem  34496  ftc2nc  34507  areaquad  39308  isosctrlem1ALT  40807  lefldiveq  41100  eliccelioc  41339  iccintsng  41341  eliccnelico  41347  eliccelicod  41348  inficc  41352  iccdificc  41357  iccleubd  41366  cncfiooiccre  41719  itgioocnicc  41803  itgspltprt  41805  itgiccshift  41806  fourierdlem1  41935  fourierdlem20  41954  fourierdlem24  41958  fourierdlem25  41959  fourierdlem27  41961  fourierdlem43  41977  fourierdlem44  41978  fourierdlem50  41983  fourierdlem51  41984  fourierdlem52  41985  fourierdlem64  41997  fourierdlem73  42006  fourierdlem76  42009  fourierdlem79  42012  fourierdlem81  42014  fourierdlem92  42025  fourierdlem102  42035  fourierdlem103  42036  fourierdlem104  42037  fourierdlem114  42047  rrxsnicc  42127  salgencntex  42168  sge0p1  42238  hoidmv1lelem3  42417  hoidmvlelem1  42419  hoidmvlelem4  42422