Theorem leidd 11680

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 11206	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ≤ 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ≤ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2111   class class class wbr 5091  ℝcr 11002   ≤ cle 11144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668  ax-resscn 11060  ax-pre-lttri 11077

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11145  df-mnf 11146  df-xr 11147  df-ltxr 11148  df-le 11149

This theorem is referenced by:  zextle  12543  uzind  12562  uzid  12744  ifle  13093  supxrre  13223  infxrre  13233  nn0fz0  13522  fvinim0ffz  13686  flid  13709  modabs2  13806  monoord  13936  leexp2r  14078  facwordi  14193  faclbnd6  14203  pfxsuffeqwrdeq  14602  repswcshw  14716  iseraltlem2  15587  climcndslem1  15753  cvgrat  15787  eirrlem  16110  ruclem2  16138  ruclem9  16144  sadcaddlem  16365  nn0seqcvgd  16478  eulerthlem2  16690  pcidlem  16781  pc2dvds  16788  pcprmpw2  16791  pcmpt  16801  ramub1lem2  16936  prmolefac  16955  prmgaplem4  16963  pgpfi  19515  zntoslem  21491  psrridm  21898  methaus  24433  nmoid  24655  xrsxmet  24723  reconnlem1  24740  metdstri  24765  nmoleub3  25044  ovolctb  25416  ovolicc1  25442  volcn  25532  mbflimsup  25592  mbfi1fseqlem4  25644  itg2const2  25667  itg2uba  25669  itg2splitlem  25674  itg2cnlem1  25687  itg2cnlem2  25688  iblss  25731  itgless  25743  itgsplitioo  25764  dvge0  25936  dvcvx  25950  dvfsumlem2  25958  dvfsumlem2OLD  25959  dvfsumlem3  25960  dvfsumrlim  25963  coe1mul4  26030  deg1mul2  26044  ply1divex  26067  deg1submon1p  26083  coe1termlem  26188  dgradd2  26199  dgrco  26206  aaliou3lem2  26276  abelth2  26377  jensen  26924  logexprlim  27161  bcmono  27213  bcmax  27214  dchrisum0flblem1  27444  pntleml  27547  eupth2  30214  blocnilem  30779  wrdt2ind  32929  fiunelros  34182  dstfrvunirn  34483  ballotlemsi  34523  dnibndlem2  36512  knoppndvlem15  36559  relowlssretop  37396  poimirlem28  37687  mblfinlem2  37697  itg2addnclem  37710  itg2gt0cn  37714  ftc1anclem7  37738  ftc1anclem8  37739  ftc1anc  37740  ssbnd  37827  bfplem1  37861  lcmineqlem4  42064  3lexlogpow5ineq2  42087  intlewftc  42093  aks4d1p1p2  42102  aks4d1p1p4  42103  dvle2  42104  aks4d1p1p6  42105  aks4d1p1p7  42106  aks4d1p1p5  42107  aks4d1p1  42108  aks4d1p3  42110  aks4d1p7d1  42114  aks4d1p7  42115  aks4d1p8  42119  aks4d1p9  42120  posbezout  42132  aks6d1c1  42148  aks6d1c2lem4  42159  aks6d1c5lem2  42170  deg1gprod  42172  sticksstones10  42187  sticksstones12a  42189  sticksstones12  42190  sticksstones22  42200  aks6d1c6lem4  42205  aks6d1c7lem1  42212  aks6d1c7lem2  42213  unitscyglem2  42228  unitscyglem4  42230  fltnlta  42695  acongeq  43015  expdiophlem1  43053  hbt  43162  dvgrat  44344  ssinc  45123  ssdec  45124  uzublem  45467  fmul01  45619  fmul01lt1lem1  45623  limciccioolb  45660  climxrre  45787  ioccncflimc  45922  icocncflimc  45926  cncfiooicclem1  45930  dvnmul  45980  iblspltprt  46010  itgspltprt  46016  stoweidlem20  46057  stoweidlem51  46088  wallispilem3  46104  fourierdlem10  46154  fourierdlem11  46155  fourierdlem14  46158  fourierdlem17  46161  fourierdlem32  46176  fourierdlem33  46177  fourierdlem41  46185  fourierdlem46  46189  fourierdlem48  46191  fourierdlem49  46192  fourierdlem50  46193  fourierdlem73  46216  fourierdlem76  46219  fourierdlem79  46222  fourierdlem93  46236  fourierdlem102  46245  fourierdlem103  46246  fourierdlem104  46247  fourierdlem107  46250  fourierdlem111  46254  fourierdlem114  46257  etransclem23  46294  rrxsnicc  46337  hsphoidmvle2  46622  hsphoidmvle  46623  hoidmv1lelem1  46628  hoidmv1lelem2  46629  hoidmv1lelem3  46630  hoidmvlelem1  46632  hoidifhspdmvle  46657  ovolval4lem2  46687  iinhoiicc  46711  vonicclem2  46721  2leaddle2  47328  bgoldbachlt  47843  logbpw2m1  48598  dignn0ldlem  48633