MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  leidd Structured version   Unicode version

Theorem leidd 10118
Description: 'Less than or equal to' is reflexive. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
leidd.1  |-  ( ph  ->  A  e.  RR )
Assertion
Ref Expression
leidd  |-  ( ph  ->  A  <_  A )

Proof of Theorem leidd
StepHypRef Expression
1 leidd.1 . 2  |-  ( ph  ->  A  e.  RR )
2 leid 9679 . 2  |-  ( A  e.  RR  ->  A  <_  A )
31, 2syl 16 1  |-  ( ph  ->  A  <_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   class class class wbr 4447   RRcr 9490    <_ cle 9628
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6575  ax-resscn 9548  ax-pre-lttri 9565
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5550  df-fun 5589  df-fn 5590  df-f 5591  df-f1 5592  df-fo 5593  df-f1o 5594  df-fv 5595  df-er 7311  df-en 7517  df-dom 7518  df-sdom 7519  df-pnf 9629  df-mnf 9630  df-xr 9631  df-ltxr 9632  df-le 9633
This theorem is referenced by:  zextle  10933  uzind  10951  uzid  11095  ifle  11395  supxrre  11518  infmxrre  11526  nn0fz0  11772  injresinjlem  11892  flid  11912  modabs2  11997  monoord  12104  leexp2r  12190  facwordi  12334  faclbnd6  12344  2swrdeqwrdeq  12640  swrdccatid  12684  repswcshw  12742  iseraltlem2  13467  climcndslem1  13623  cvgrat  13654  eirrlem  13797  ruclem2  13825  ruclem9  13831  sadcaddlem  13965  nn0seqcvgd  14057  eulerthlem2  14170  pcidlem  14253  pc2dvds  14260  pcprmpw2  14263  pcmpt  14269  ramub1lem2  14403  pgpfi  16428  psrridm  17845  psrridmOLD  17846  zntoslem  18378  methaus  20774  nmoid  21000  xrsxmet  21065  reconnlem1  21082  metdstri  21106  nmoleub3  21353  ovolctb  21652  ovolicc1  21678  volcn  21766  mbflimsup  21824  mbfi1fseqlem4  21876  itg2const2  21899  itg2uba  21901  itg2splitlem  21906  itg2cnlem1  21919  itg2cnlem2  21920  iblss  21962  itgless  21974  itgsplitioo  21995  dvge0  22158  dvcvx  22172  dvfsumlem2  22179  dvfsumlem3  22180  dvfsumrlim  22183  coe1mul4  22252  deg1mul2  22266  ply1divex  22288  deg1submon1p  22304  coe1termlem  22405  dgradd2  22415  dgrco  22422  aaliou3lem2  22489  abelth2  22587  jensen  23062  logexprlim  23244  bcmono  23296  bcmax  23297  dchrisum0flblem1  23437  pntleml  23540  wlkonwlk  24229  cyclnspth  24323  eupath2  24672  blocnilem  25411  dstfrvunirn  28069  ballotlemsi  28109  mblfinlem2  29645  itg2addnclem  29659  itg2gt0cn  29663  ftc1anclem7  29689  ftc1anclem8  29690  ftc1anc  29691  ssbnd  29903  bfplem1  29937  acongeq  30541  expdiophlem1  30583  hbt  30699  fmul01  31146  fmul01lt1lem1  31150  limciccioolb  31179  ioccncflimc  31240  icocncflimc  31244  cncfiooicclem1  31248  ioodvbdlimc2lem  31280  iblspltprt  31307  itgspltprt  31313  stoweidlem20  31336  stoweidlem51  31367  wallispilem3  31383  fourierdlem10  31433  fourierdlem11  31434  fourierdlem14  31437  fourierdlem17  31440  fourierdlem32  31455  fourierdlem33  31456  fourierdlem41  31464  fourierdlem46  31469  fourierdlem48  31471  fourierdlem49  31472  fourierdlem50  31473  fourierdlem73  31496  fourierdlem76  31499  fourierdlem79  31502  fourierdlem93  31516  fourierdlem102  31525  fourierdlem103  31526  fourierdlem104  31527  fourierdlem107  31530  fourierdlem111  31534  fourierdlem114  31537  2leaddle2  31803
  Copyright terms: Public domain W3C validator