Theorem iccleub 11692

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	|- ( ( A e. RR* /\ B e. RR* /\ C e. ( A [,] B ) ) -> C <_ B )

Proof of Theorem iccleub

Step	Hyp	Ref	Expression
1		elicc1 11682	. . 3 |- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A [,] B ) <-> ( C e. RR* /\ A <_ C /\ C <_ B ) ) )
2		simp3 1008	. . 3 |- ( ( C e. RR* /\ A <_ C /\ C <_ B ) -> C <_ B )
3	1, 2	syl6bi 232	. 2 |- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A [,] B ) -> C <_ B ) )
4	3	3impia 1203	1 |- ( ( A e. RR* /\ B e. RR* /\ C e. ( A [,] B ) ) -> C <_ B )

Syntax hints:   -> wi 4   /\ wa 371   /\ w3a 983   e. wcel 1869   class class class wbr 4421  (class class class)co 6303   RR*cxr 9676   <_ cle 9678   [,]cicc 11640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pr 4658  ax-un 6595  ax-cnex 9597  ax-resscn 9598

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-sbc 3301  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-br 4422  df-opab 4481  df-id 4766  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-iota 5563  df-fun 5601  df-fv 5607  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-xr 9681  df-icc 11644

This theorem is referenced by:  supicc  11782  supiccub  11783  supicclub  11784  oprpiece1res1  21971  ivthlem1  22394  isosctrlem1  23739  ttgcontlem1  24907  broucube  31932  mblfinlem1  31935  ftc1cnnclem  31973  ftc2nc  31984  areaquad  36065  isosctrlem1ALT  37236  lefldiveq  37392  eliccelioc  37497  iccintsng  37499  eliccnelico  37506  eliccelicod  37507  inficc  37510  cncfiooiccre  37637  itgioocnicc  37718  itgspltprt  37720  itgiccshift  37721  fourierdlem1  37834  fourierdlem20  37853  fourierdlem24  37857  fourierdlem25  37858  fourierdlem27  37860  fourierdlem43  37878  fourierdlem44  37879  fourierdlem50  37884  fourierdlem51  37885  fourierdlem52  37886  fourierdlem64  37898  fourierdlem73  37907  fourierdlem76  37910  fourierdlem79  37913  fourierdlem81  37915  fourierdlem92  37926  fourierdlem102  37936  fourierdlem103  37937  fourierdlem104  37938  fourierdlem114  37948  sge0p1  38088