Theorem leidd 11780

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

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5149  ℝcr 11109   ≤ cle 11249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-resscn 11167  ax-pre-lttri 11184

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254

This theorem is referenced by:  zextle  12635  uzind  12654  uzid  12837  ifle  13176  supxrre  13306  infxrre  13315  nn0fz0  13599  fvinim0ffz  13751  flid  13773  modabs2  13870  monoord  13998  leexp2r  14139  facwordi  14249  faclbnd6  14259  pfxsuffeqwrdeq  14648  repswcshw  14762  iseraltlem2  15629  climcndslem1  15795  cvgrat  15829  eirrlem  16147  ruclem2  16175  ruclem9  16181  sadcaddlem  16398  nn0seqcvgd  16507  eulerthlem2  16715  pcidlem  16805  pc2dvds  16812  pcprmpw2  16815  pcmpt  16825  ramub1lem2  16960  prmolefac  16979  prmgaplem4  16987  pgpfi  19473  zntoslem  21112  psrridm  21524  methaus  24029  nmoid  24259  xrsxmet  24325  reconnlem1  24342  metdstri  24367  nmoleub3  24635  ovolctb  25007  ovolicc1  25033  volcn  25123  mbflimsup  25183  mbfi1fseqlem4  25236  itg2const2  25259  itg2uba  25261  itg2splitlem  25266  itg2cnlem1  25279  itg2cnlem2  25280  iblss  25322  itgless  25334  itgsplitioo  25355  dvge0  25523  dvcvx  25537  dvfsumlem2  25544  dvfsumlem3  25545  dvfsumrlim  25548  coe1mul4  25618  deg1mul2  25632  ply1divex  25654  deg1submon1p  25670  coe1termlem  25772  dgradd2  25782  dgrco  25789  aaliou3lem2  25856  abelth2  25954  jensen  26493  logexprlim  26728  bcmono  26780  bcmax  26781  dchrisum0flblem1  27011  pntleml  27114  eupth2  29492  blocnilem  30057  wrdt2ind  32117  fiunelros  33172  dstfrvunirn  33473  ballotlemsi  33513  gg-dvfsumlem2  35183  dnibndlem2  35355  knoppndvlem15  35402  relowlssretop  36244  poimirlem28  36516  mblfinlem2  36526  itg2addnclem  36539  itg2gt0cn  36543  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  ssbnd  36656  bfplem1  36690  lcmineqlem4  40897  3lexlogpow5ineq2  40920  intlewftc  40926  aks4d1p1p2  40935  aks4d1p1p4  40936  dvle2  40937  aks4d1p1p6  40938  aks4d1p1p7  40939  aks4d1p1p5  40940  aks4d1p1  40941  aks4d1p3  40943  aks4d1p7d1  40947  aks4d1p7  40948  aks4d1p8  40952  aks4d1p9  40953  sticksstones10  40971  sticksstones12a  40973  sticksstones12  40974  sticksstones22  40984  metakunt1  40985  metakunt10  40994  metakunt24  41008  metakunt26  41010  2xp3dxp2ge1d  41022  fltnlta  41405  acongeq  41722  expdiophlem1  41760  hbt  41872  dvgrat  43071  ssinc  43776  ssdec  43777  uzublem  44140  fmul01  44296  fmul01lt1lem1  44300  limciccioolb  44337  climxrre  44466  ioccncflimc  44601  icocncflimc  44605  cncfiooicclem1  44609  dvnmul  44659  iblspltprt  44689  itgspltprt  44695  stoweidlem20  44736  stoweidlem51  44767  wallispilem3  44783  fourierdlem10  44833  fourierdlem11  44834  fourierdlem14  44837  fourierdlem17  44840  fourierdlem32  44855  fourierdlem33  44856  fourierdlem41  44864  fourierdlem46  44868  fourierdlem48  44870  fourierdlem49  44871  fourierdlem50  44872  fourierdlem73  44895  fourierdlem76  44898  fourierdlem79  44901  fourierdlem93  44915  fourierdlem102  44924  fourierdlem103  44925  fourierdlem104  44926  fourierdlem107  44929  fourierdlem111  44933  fourierdlem114  44936  etransclem23  44973  rrxsnicc  45016  hsphoidmvle2  45301  hsphoidmvle  45302  hoidmv1lelem1  45307  hoidmv1lelem2  45308  hoidmv1lelem3  45309  hoidmvlelem1  45311  hoidifhspdmvle  45336  ovolval4lem2  45366  iinhoiicc  45390  vonicclem2  45400  2leaddle2  46006  bgoldbachlt  46481  logbpw2m1  47253  dignn0ldlem  47288