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

Theorem leidd 10126
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 9683 . 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 1804   class class class wbr 4437   RRcr 9494    <_ cle 9632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-resscn 9552  ax-pre-lttri 9569
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637
This theorem is referenced by:  zextle  10943  uzind  10961  uzid  11106  ifle  11407  supxrre  11530  infmxrre  11538  nn0fz0  11785  injresinjlem  11907  flid  11927  modabs2  12012  monoord  12119  leexp2r  12205  facwordi  12349  faclbnd6  12359  2swrdeqwrdeq  12660  swrdccatid  12704  repswcshw  12762  iseraltlem2  13487  climcndslem1  13643  cvgrat  13674  eirrlem  13919  ruclem2  13947  ruclem9  13953  sadcaddlem  14089  nn0seqcvgd  14181  eulerthlem2  14294  pcidlem  14377  pc2dvds  14384  pcprmpw2  14387  pcmpt  14393  ramub1lem2  14527  pgpfi  16604  psrridm  18037  psrridmOLD  18038  zntoslem  18573  methaus  21001  nmoid  21227  xrsxmet  21292  reconnlem1  21309  metdstri  21333  nmoleub3  21580  ovolctb  21879  ovolicc1  21905  volcn  21993  mbflimsup  22051  mbfi1fseqlem4  22103  itg2const2  22126  itg2uba  22128  itg2splitlem  22133  itg2cnlem1  22146  itg2cnlem2  22147  iblss  22189  itgless  22201  itgsplitioo  22222  dvge0  22385  dvcvx  22399  dvfsumlem2  22406  dvfsumlem3  22407  dvfsumrlim  22410  coe1mul4  22479  deg1mul2  22493  ply1divex  22515  deg1submon1p  22531  coe1termlem  22633  dgradd2  22643  dgrco  22650  aaliou3lem2  22717  abelth2  22815  jensen  23296  logexprlim  23478  bcmono  23530  bcmax  23531  dchrisum0flblem1  23671  pntleml  23774  wlkonwlk  24515  cyclnspth  24609  eupath2  24958  blocnilem  25697  dstfrvunirn  28391  ballotlemsi  28431  mblfinlem2  30028  itg2addnclem  30042  itg2gt0cn  30046  ftc1anclem7  30072  ftc1anclem8  30073  ftc1anc  30074  ssbnd  30260  bfplem1  30294  acongeq  30897  expdiophlem1  30939  hbt  31055  dvgrat  31169  fmul01  31528  fmul01lt1lem1  31532  limciccioolb  31581  ioccncflimc  31642  icocncflimc  31646  cncfiooicclem1  31650  dvnmul  31694  iblspltprt  31726  itgspltprt  31732  stoweidlem20  31756  stoweidlem51  31787  wallispilem3  31803  fourierdlem10  31853  fourierdlem11  31854  fourierdlem14  31857  fourierdlem17  31860  fourierdlem32  31875  fourierdlem33  31876  fourierdlem41  31884  fourierdlem46  31889  fourierdlem48  31891  fourierdlem49  31892  fourierdlem50  31893  fourierdlem73  31916  fourierdlem76  31919  fourierdlem79  31922  fourierdlem93  31936  fourierdlem102  31945  fourierdlem103  31946  fourierdlem104  31947  fourierdlem107  31950  fourierdlem111  31954  fourierdlem114  31957  etransclem23  31994  2leaddle2  32274
  Copyright terms: Public domain W3C validator