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

Theorem leidd 9906
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 9470 . 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 1756   class class class wbr 4292   RRcr 9281    <_ cle 9419
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 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372  ax-resscn 9339  ax-pre-lttri 9356
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 2568  df-ne 2608  df-nel 2609  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-er 7101  df-en 7311  df-dom 7312  df-sdom 7313  df-pnf 9420  df-mnf 9421  df-xr 9422  df-ltxr 9423  df-le 9424
This theorem is referenced by:  zextle  10715  uzind  10733  uzid  10875  ifle  11167  supxrre  11290  infmxrre  11298  nn0fz0  11525  injresinjlem  11638  flid  11657  modabs2  11742  monoord  11836  leexp2r  11921  facwordi  12065  faclbnd6  12075  2swrdeqwrdeq  12347  swrdccatid  12388  repswcshw  12446  iseraltlem2  13160  climcndslem1  13312  cvgrat  13343  eirrlem  13486  ruclem2  13514  ruclem9  13520  sadcaddlem  13653  nn0seqcvgd  13745  eulerthlem2  13857  pcidlem  13938  pc2dvds  13945  pcprmpw2  13948  pcmpt  13954  ramub1lem2  14088  pgpfi  16104  psrridm  17476  psrridmOLD  17477  zntoslem  17989  methaus  20095  nmoid  20321  xrsxmet  20386  reconnlem1  20403  metdstri  20427  nmoleub3  20674  ovolctb  20973  ovolicc1  20999  volcn  21086  mbflimsup  21144  mbfi1fseqlem4  21196  itg2const2  21219  itg2uba  21221  itg2splitlem  21226  itg2cnlem1  21239  itg2cnlem2  21240  iblss  21282  itgless  21294  itgsplitioo  21315  dvge0  21478  dvcvx  21492  dvfsumlem2  21499  dvfsumlem3  21500  dvfsumrlim  21503  coe1mul4  21572  deg1mul2  21586  ply1divex  21608  deg1submon1p  21624  coe1termlem  21725  dgradd2  21735  dgrco  21742  aaliou3lem2  21809  abelth2  21907  jensen  22382  logexprlim  22564  bcmono  22616  bcmax  22617  dchrisum0flblem1  22757  pntleml  22860  wlkonwlk  23434  cyclnspth  23517  eupath2  23601  blocnilem  24204  dstfrvunirn  26857  ballotlemsi  26897  mblfinlem2  28429  itg2addnclem  28443  itg2gt0cn  28447  ftc1anclem7  28473  ftc1anclem8  28474  ftc1anc  28475  ssbnd  28687  bfplem1  28721  acongeq  29326  expdiophlem1  29370  hbt  29486  fmul01  29761  fmul01lt1lem1  29765  stoweidlem20  29815  stoweidlem51  29846  wallispilem3  29862  2leaddle2  30175
  Copyright terms: Public domain W3C validator