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

Theorem leidd 11722
Description: 'Less than or equal to' is reflexive. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
leidd.1 (𝜑𝐴 ∈ ℝ)
Assertion
Ref Expression
leidd (𝜑𝐴𝐴)

Proof of Theorem leidd
StepHypRef Expression
1 leidd.1 . 2 (𝜑𝐴 ∈ ℝ)
2 leid 11252 . 2 (𝐴 ∈ ℝ → 𝐴𝐴)
31, 2syl 17 1 (𝜑𝐴𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107   class class class wbr 5106  cr 11051  cle 11191
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-resscn 11109  ax-pre-lttri 11126
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-er 8649  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11192  df-mnf 11193  df-xr 11194  df-ltxr 11195  df-le 11196
This theorem is referenced by:  zextle  12577  uzind  12596  uzid  12779  ifle  13117  supxrre  13247  infxrre  13256  nn0fz0  13540  fvinim0ffz  13692  flid  13714  modabs2  13811  monoord  13939  leexp2r  14080  facwordi  14190  faclbnd6  14200  pfxsuffeqwrdeq  14587  repswcshw  14701  iseraltlem2  15568  climcndslem1  15735  cvgrat  15769  eirrlem  16087  ruclem2  16115  ruclem9  16121  sadcaddlem  16338  nn0seqcvgd  16447  eulerthlem2  16655  pcidlem  16745  pc2dvds  16752  pcprmpw2  16755  pcmpt  16765  ramub1lem2  16900  prmolefac  16919  prmgaplem4  16927  pgpfi  19388  zntoslem  20966  psrridm  21376  methaus  23879  nmoid  24109  xrsxmet  24175  reconnlem1  24192  metdstri  24217  nmoleub3  24485  ovolctb  24857  ovolicc1  24883  volcn  24973  mbflimsup  25033  mbfi1fseqlem4  25086  itg2const2  25109  itg2uba  25111  itg2splitlem  25116  itg2cnlem1  25129  itg2cnlem2  25130  iblss  25172  itgless  25184  itgsplitioo  25205  dvge0  25373  dvcvx  25387  dvfsumlem2  25394  dvfsumlem3  25395  dvfsumrlim  25398  coe1mul4  25468  deg1mul2  25482  ply1divex  25504  deg1submon1p  25520  coe1termlem  25622  dgradd2  25632  dgrco  25639  aaliou3lem2  25706  abelth2  25804  jensen  26341  logexprlim  26576  bcmono  26628  bcmax  26629  dchrisum0flblem1  26859  pntleml  26962  eupth2  29186  blocnilem  29749  wrdt2ind  31810  fiunelros  32776  dstfrvunirn  33077  ballotlemsi  33117  dnibndlem2  34945  knoppndvlem15  34992  relowlssretop  35837  poimirlem28  36109  mblfinlem2  36119  itg2addnclem  36132  itg2gt0cn  36136  ftc1anclem7  36160  ftc1anclem8  36161  ftc1anc  36162  ssbnd  36250  bfplem1  36284  lcmineqlem4  40492  3lexlogpow5ineq2  40515  intlewftc  40521  aks4d1p1p2  40530  aks4d1p1p4  40531  dvle2  40532  aks4d1p1p6  40533  aks4d1p1p7  40534  aks4d1p1p5  40535  aks4d1p1  40536  aks4d1p3  40538  aks4d1p7d1  40542  aks4d1p7  40543  aks4d1p8  40547  aks4d1p9  40548  sticksstones10  40566  sticksstones12a  40568  sticksstones12  40569  sticksstones22  40579  metakunt1  40580  metakunt10  40589  metakunt24  40603  metakunt26  40605  2xp3dxp2ge1d  40617  fltnlta  41004  acongeq  41310  expdiophlem1  41348  hbt  41460  dvgrat  42599  ssinc  43304  ssdec  43305  uzublem  43672  fmul01  43828  fmul01lt1lem1  43832  limciccioolb  43869  climxrre  43998  ioccncflimc  44133  icocncflimc  44137  cncfiooicclem1  44141  dvnmul  44191  iblspltprt  44221  itgspltprt  44227  stoweidlem20  44268  stoweidlem51  44299  wallispilem3  44315  fourierdlem10  44365  fourierdlem11  44366  fourierdlem14  44369  fourierdlem17  44372  fourierdlem32  44387  fourierdlem33  44388  fourierdlem41  44396  fourierdlem46  44400  fourierdlem48  44402  fourierdlem49  44403  fourierdlem50  44404  fourierdlem73  44427  fourierdlem76  44430  fourierdlem79  44433  fourierdlem93  44447  fourierdlem102  44456  fourierdlem103  44457  fourierdlem104  44458  fourierdlem107  44461  fourierdlem111  44465  fourierdlem114  44468  etransclem23  44505  rrxsnicc  44548  hsphoidmvle2  44833  hsphoidmvle  44834  hoidmv1lelem1  44839  hoidmv1lelem2  44840  hoidmv1lelem3  44841  hoidmvlelem1  44843  hoidifhspdmvle  44868  ovolval4lem2  44898  iinhoiicc  44922  vonicclem2  44932  2leaddle2  45537  bgoldbachlt  46012  logbpw2m1  46660  dignn0ldlem  46695
  Copyright terms: Public domain W3C validator