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

Theorem leidd 9585
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 9161 . 2  |-  ( A  e.  RR  ->  A  <_  A )
31, 2syl 16 1  |-  ( ph  ->  A  <_  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   class class class wbr 4204   RRcr 8981    <_ cle 9113
This theorem is referenced by:  zextle  10335  uzind  10353  uzid  10492  ifle  10775  supxrre  10898  infmxrre  10906  nn0fz0  11106  injresinjlem  11191  flid  11208  modabs2  11267  monoord  11345  leexp2r  11429  facwordi  11572  faclbnd6  11582  iseraltlem2  12468  climcndslem1  12621  cvgrat  12652  eirrlem  12795  ruclem2  12823  ruclem9  12829  sadcaddlem  12961  nn0seqcvgd  13053  eulerthlem2  13163  pcidlem  13237  pc2dvds  13244  pcprmpw2  13247  pcmpt  13253  ramub1lem2  13387  pgpfi  15231  psrridm  16460  zntoslem  16829  methaus  18542  nmoid  18768  xrsxmet  18832  reconnlem1  18849  metdstri  18873  nmoleub3  19119  ovolctb  19378  ovolicc1  19404  volcn  19490  mbflimsup  19550  mbfi1fseqlem4  19602  itg2const2  19625  itg2uba  19627  itg2splitlem  19632  itg2cnlem1  19645  itg2cnlem2  19646  iblss  19688  itgless  19700  itgsplitioo  19721  dvge0  19882  dvcvx  19896  dvfsumlem2  19903  dvfsumlem3  19904  dvfsumrlim  19907  coe1mul4  20015  deg1mul2  20029  ply1divex  20051  deg1submon1p  20067  coe1termlem  20168  dgradd2  20178  dgrco  20185  aaliou3lem2  20252  abelth2  20350  jensen  20819  logexprlim  21001  bcmono  21053  bcmax  21054  dchrisum0flblem1  21194  pntleml  21297  wlkonwlk  21527  cyclnspth  21610  eupath2  21694  blocnilem  22297  dstfrvunirn  24724  ballotlemsi  24764  mblfinlem  26234  itg2addnclem  26246  itg2gt0cn  26250  ftc1anclem7  26276  ftc1anclem8  26277  ftc1anc  26278  ssbnd  26488  bfplem1  26522  acongeq  27039  expdiophlem1  27083  hbt  27302  fmul01  27677  fmul01lt1lem1  27681  stoweidlem20  27736  stoweidlem51  27767  wallispilem3  27783  2leaddle2  28077  cshwlen  28207  2cshw1lem1  28214  2cshwid  28224  cshweqdif2  28233
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-resscn 9039  ax-pre-lttri 9056
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-er 6897  df-en 7102  df-dom 7103  df-sdom 7104  df-pnf 9114  df-mnf 9115  df-xr 9116  df-ltxr 9117  df-le 9118
  Copyright terms: Public domain W3C validator