Theorem iccleub 13444

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2146   class class class wbr 5111  (class class class)co 7419  ℝ^*cxr 11257   ≤ cle 11259  [,]cicc 13391

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-pr 5406  ax-un 7742  ax-cnex 11171  ax-resscn 11172

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6496  df-fun 6542  df-fv 6548  df-ov 7422  df-oprab 7423  df-mpo 7424  df-xr 11262  df-icc 13395

This theorem is used by:  supicc  13544  supiccub  13545  supicclub  13546  oprpiece1res1  25161  ivthlem1  25661  isosctrlem1  27034  ttgcontlem1  29289  broucube  38362  mblfinlem1  38365  ftc1cnnclem  38399  ftc2nc  38410  areaquad  44001  isosctrlem1ALT  45700  lefldiveq  46069  eliccelioc  46295  iccintsng  46297  eliccnelico  46303  eliccelicod  46304  inficc  46308  iccdificc  46313  iccleubd  46322  cncfiooiccre  46667  itgioocnicc  46749  itgspltprt  46751  itgiccshift  46752  fourierdlem1  46880  fourierdlem20  46899  fourierdlem24  46903  fourierdlem25  46904  fourierdlem27  46906  fourierdlem43  46922  fourierdlem44  46923  fourierdlem50  46928  fourierdlem51  46929  fourierdlem52  46930  fourierdlem64  46942  fourierdlem73  46951  fourierdlem76  46954  fourierdlem79  46957  fourierdlem81  46959  fourierdlem92  46970  fourierdlem102  46980  fourierdlem103  46981  fourierdlem104  46982  fourierdlem114  46992  rrxsnicc  47072  salgencntex  47115  sge0p1  47186  hoidmv1lelem3  47365  hoidmvlelem1  47367  hoidmvlelem4  47370