Theorem ltle 9466

Description: 'Less than' implies 'less than or equal to'. (Contributed by NM, 25-Aug-1999.)

Assertion

Ref	Expression
ltle	|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> A <_ B ) )

Proof of Theorem ltle

Step	Hyp	Ref	Expression
1		orc 385	. 2 |- ( A < B -> ( A < B \/ A = B ) )
2		leloe 9464	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> ( A < B \/ A = B ) ) )
3	1, 2	syl5ibr 221	1 |- ( ( A e. RR /\ B e. RR ) -> ( A < B -> A <_ B ) )

Syntax hints:   -> wi 4   \/ wo 368   /\ wa 369   = wceq 1369   e. wcel 1756   class class class wbr 4295   RRcr 9284   < clt 9421   <_ cle 9422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4416  ax-nul 4424  ax-pow 4473  ax-pr 4534  ax-un 6375  ax-resscn 9342  ax-pre-lttri 9359

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-nel 2612  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-sbc 3190  df-csb 3292  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-pw 3865  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-br 4296  df-opab 4354  df-mpt 4355  df-id 4639  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-res 4855  df-ima 4856  df-iota 5384  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-er 7104  df-en 7314  df-dom 7315  df-sdom 7316  df-pnf 9423  df-mnf 9424  df-xr 9425  df-ltxr 9426  df-le 9427

This theorem is referenced by:  ltleletr  9470  letr  9471  letric  9478  ltlen  9479  ltlei  9499  ltled  9525  lt2add  9827  lep1  10171  lem1  10173  letrp1  10174  ltmul12a  10188  mulge0b  10202  lediv12a  10228  bndndx  10581  uzind  10736  fnn0ind  10744  eluz2b2  10930  lbzbi  10946  zmin  10952  rpnnen1lem1  10982  rpnnen1lem2  10983  rpnnen1lem3  10984  rpnnen1lem5  10986  rpge0  11006  rpneg  11023  iccsplit  11421  elfzouz2  11569  elfzo0le  11593  fzostep1  11638  fllep1  11654  fracle1  11656  expgt1  11905  expnbnd  11996  expnlbnd2  11998  faclbnd  12069  swrdccat3  12386  repswswrd  12425  resqrex  12743  sqrgt0  12751  absmax  12820  eqsqr2d  12859  rlim2lt  12978  mulcn2  13076  rlimo1  13097  o1rlimmul  13099  climbdd  13152  caucvgrlem  13153  supcvg  13321  efcllem  13366  sin01bnd  13472  cos01bnd  13473  sin01gt0  13477  cos01gt0  13478  absef  13484  efieq1re  13486  ruclem11  13525  pythagtriplem12  13896  pythagtriplem13  13897  pythagtriplem14  13898  pythagtriplem16  13900  pclem  13908  cshwshashlem2  14126  isabvd  16908  met2ndci  20100  blcvx  20378  icoopnst  20514  iocopnst  20515  nmoleub2a  20675  nmoleub2b  20676  nmhmcn  20678  iscmet3lem2  20806  caubl  20821  ivthlem2  20939  ovolicc2lem4  21006  ioombl1lem4  21045  ioovolcl  21053  volsup2  21088  itg2monolem1  21231  itg2gt0  21241  itg2cnlem1  21242  dvne0  21486  ftc1lem4  21514  dgrlt  21736  aalioulem5  21805  ulmbdd  21866  iblulm  21875  radcnvlem1  21881  abelthlem5  21903  abelthlem7  21906  sincosq1lem  21962  tangtx  21970  tanabsge  21971  sinq12ge0  21973  sineq0  21986  tanord  21997  logcj  22058  argregt0  22062  argrege0  22063  argimgt0  22064  logdmnrp  22089  logcnlem3  22092  logf1o2  22098  cxpsqrlem  22150  abscxpbnd  22194  logreclem  22217  asinneg  22284  atanlogsublem  22313  atanlogsub  22314  rlimcnp  22362  xrlimcnp  22365  basellem8  22428  chtub  22554  bposlem9  22634  chebbnd1  22724  chtppilimlem1  22725  dchrvmasumiflem1  22753  mulog2sumlem2  22787  pntrmax  22816  pntibndlem2  22843  pntibndlem3  22844  pntlemf  22857  axlowdimlem16  23206  nmblolbii  24202  ubthlem1  24274  bcsiALT  24584  nmbdoplbi  25431  nmcexi  25433  nmcoplbi  25435  lnconi  25440  nmbdfnlbi  25456  nmcfnlbi  25459  nmopcoi  25502  branmfn  25512  leopmul  25541  nmopleid  25546  esumcvg  26538  ballotlemfrceq  26914  sinccvglem  27320  ltflcei  28422  ftc1cnnclem  28468  ftc1anclem5  28474  opnrebl2  28519  ivthALT  28533  incsequz2  28648  nnubfi  28649  bfplem2  28725  pell14qrgap  29219  pellfundre  29225  pellfundlb  29228  stoweidlem17  29815  stoweidlem34  29832  wallispilem1  29863  leltletr  30176  ltsubnn0  30185  2elfz2melfz  30205  elfzelfzlble  30212  subsubelfzo0  30213  fzosplitprm1  30227  difelfznle  30491