Theorem leidd 11708

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

Step	Hyp	Ref	Expression
1		leidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		leid 11234	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ≤ 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ≤ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2119   class class class wbr 5073  ℝcr 11029   ≤ cle 11172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5219  ax-nul 5229  ax-pow 5295  ax-pr 5363  ax-un 7679  ax-resscn 11087  ax-pre-lttri 11104

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4263  df-if 4456  df-pw 4532  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4840  df-br 5074  df-opab 5136  df-mpt 5155  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11173  df-mnf 11174  df-xr 11175  df-ltxr 11176  df-le 11177

This theorem is referenced by:  zextle  12594  uzind  12613  uzid  12795  ifle  13141  supxrre  13271  infxrre  13281  nn0fz0  13571  fvinim0ffz  13736  flid  13759  modabs2  13856  monoord  13986  leexp2r  14128  facwordi  14243  faclbnd6  14253  pfxsuffeqwrdeq  14652  repswcshw  14766  iseraltlem2  15637  climcndslem1  15806  cvgrat  15840  eirrlem  16163  ruclem2  16191  ruclem9  16197  sadcaddlem  16418  nn0seqcvgd  16531  eulerthlem2  16744  pcidlem  16835  pc2dvds  16842  pcprmpw2  16845  pcmpt  16855  ramub1lem2  16990  prmolefac  17009  prmgaplem4  17017  pgpfi  19572  zntoslem  21532  psrridm  21938  methaus  24504  nmoid  24726  xrsxmet  24794  reconnlem1  24811  metdstri  24836  nmoleub3  25105  ovolctb  25476  ovolicc1  25502  volcn  25592  mbflimsup  25652  mbfi1fseqlem4  25704  itg2const2  25727  itg2uba  25729  itg2splitlem  25734  itg2cnlem1  25747  itg2cnlem2  25748  iblss  25791  itgless  25803  itgsplitioo  25824  dvge0  25992  dvcvx  26006  dvfsumlem2  26013  dvfsumlem3  26014  dvfsumrlim  26017  coe1mul4  26084  deg1mul2  26098  ply1divex  26121  deg1submon1p  26137  coe1termlem  26242  dgradd2  26252  dgrco  26259  aaliou3lem2  26328  abelth2  26426  jensen  26971  logexprlim  27207  bcmono  27259  bcmax  27260  dchrisum0flblem1  27490  pntleml  27593  eupth2  30328  blocnilem  30894  wrdt2ind  33033  fiunelros  34367  dstfrvunirn  34668  ballotlemsi  34708  dnibndlem2  36794  knoppndvlem15  36841  relowlssretop  37734  poimirlem28  38024  mblfinlem2  38034  itg2addnclem  38047  itg2gt0cn  38051  ftc1anclem7  38075  ftc1anclem8  38076  ftc1anc  38077  ssbnd  38164  bfplem1  38198  lcmineqlem4  42526  3lexlogpow5ineq2  42549  intlewftc  42555  aks4d1p1p2  42564  aks4d1p1p4  42565  dvle2  42566  aks4d1p1p6  42567  aks4d1p1p7  42568  aks4d1p1p5  42569  aks4d1p1  42570  aks4d1p3  42572  aks4d1p7d1  42576  aks4d1p7  42577  aks4d1p8  42581  aks4d1p9  42582  posbezout  42594  aks6d1c1  42610  aks6d1c2lem4  42621  aks6d1c5lem2  42632  deg1gprod  42634  sticksstones10  42649  sticksstones12a  42651  sticksstones12  42652  sticksstones22  42662  aks6d1c6lem4  42667  aks6d1c7lem1  42674  aks6d1c7lem2  42675  unitscyglem2  42690  unitscyglem4  42692  fltnlta  43122  acongeq  43437  expdiophlem1  43475  hbt  43584  dvgrat  44765  ssinc  45542  ssdec  45543  uzublem  45881  fmul01  46033  fmul01lt1lem1  46037  limciccioolb  46074  climxrre  46201  ioccncflimc  46336  icocncflimc  46340  cncfiooicclem1  46344  dvnmul  46394  iblspltprt  46424  itgspltprt  46430  stoweidlem20  46471  stoweidlem51  46502  wallispilem3  46518  fourierdlem10  46568  fourierdlem11  46569  fourierdlem14  46572  fourierdlem17  46575  fourierdlem32  46590  fourierdlem33  46591  fourierdlem41  46599  fourierdlem46  46603  fourierdlem48  46605  fourierdlem49  46606  fourierdlem50  46607  fourierdlem73  46630  fourierdlem76  46633  fourierdlem79  46636  fourierdlem93  46650  fourierdlem102  46659  fourierdlem103  46660  fourierdlem104  46661  fourierdlem107  46664  fourierdlem111  46668  fourierdlem114  46671  etransclem23  46708  rrxsnicc  46751  hsphoidmvle2  47036  hsphoidmvle  47037  hoidmv1lelem1  47042  hoidmv1lelem2  47043  hoidmv1lelem3  47044  hoidmvlelem1  47046  hoidifhspdmvle  47071  ovolval4lem2  47101  iinhoiicc  47125  vonicclem2  47135  2leaddle2  47769  bgoldbachlt  48312  logbpw2m1  49066  dignn0ldlem  49101