Theorem leidd 11827

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

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5148  ℝcr 11152   ≤ cle 11294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-resscn 11210  ax-pre-lttri 11227

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299

This theorem is referenced by:  zextle  12689  uzind  12708  uzid  12891  ifle  13236  supxrre  13366  infxrre  13375  nn0fz0  13662  fvinim0ffz  13822  flid  13845  modabs2  13942  monoord  14070  leexp2r  14211  facwordi  14325  faclbnd6  14335  pfxsuffeqwrdeq  14733  repswcshw  14847  iseraltlem2  15716  climcndslem1  15882  cvgrat  15916  eirrlem  16237  ruclem2  16265  ruclem9  16271  sadcaddlem  16491  nn0seqcvgd  16604  eulerthlem2  16816  pcidlem  16906  pc2dvds  16913  pcprmpw2  16916  pcmpt  16926  ramub1lem2  17061  prmolefac  17080  prmgaplem4  17088  pgpfi  19638  zntoslem  21593  psrridm  22001  methaus  24549  nmoid  24779  xrsxmet  24845  reconnlem1  24862  metdstri  24887  nmoleub3  25166  ovolctb  25539  ovolicc1  25565  volcn  25655  mbflimsup  25715  mbfi1fseqlem4  25768  itg2const2  25791  itg2uba  25793  itg2splitlem  25798  itg2cnlem1  25811  itg2cnlem2  25812  iblss  25855  itgless  25867  itgsplitioo  25888  dvge0  26060  dvcvx  26074  dvfsumlem2  26082  dvfsumlem2OLD  26083  dvfsumlem3  26084  dvfsumrlim  26087  coe1mul4  26154  deg1mul2  26168  ply1divex  26191  deg1submon1p  26207  coe1termlem  26312  dgradd2  26323  dgrco  26330  aaliou3lem2  26400  abelth2  26501  jensen  27047  logexprlim  27284  bcmono  27336  bcmax  27337  dchrisum0flblem1  27567  pntleml  27670  eupth2  30268  blocnilem  30833  wrdt2ind  32923  fiunelros  34155  dstfrvunirn  34456  ballotlemsi  34496  dnibndlem2  36462  knoppndvlem15  36509  relowlssretop  37346  poimirlem28  37635  mblfinlem2  37645  itg2addnclem  37658  itg2gt0cn  37662  ftc1anclem7  37686  ftc1anclem8  37687  ftc1anc  37688  ssbnd  37775  bfplem1  37809  lcmineqlem4  42014  3lexlogpow5ineq2  42037  intlewftc  42043  aks4d1p1p2  42052  aks4d1p1p4  42053  dvle2  42054  aks4d1p1p6  42055  aks4d1p1p7  42056  aks4d1p1p5  42057  aks4d1p1  42058  aks4d1p3  42060  aks4d1p7d1  42064  aks4d1p7  42065  aks4d1p8  42069  aks4d1p9  42070  posbezout  42082  aks6d1c1  42098  aks6d1c2lem4  42109  aks6d1c5lem2  42120  deg1gprod  42122  sticksstones10  42137  sticksstones12a  42139  sticksstones12  42140  sticksstones22  42150  aks6d1c6lem4  42155  aks6d1c7lem1  42162  aks6d1c7lem2  42163  unitscyglem2  42178  unitscyglem4  42180  metakunt1  42187  metakunt10  42196  metakunt24  42210  metakunt26  42212  2xp3dxp2ge1d  42223  fltnlta  42650  acongeq  42972  expdiophlem1  43010  hbt  43119  dvgrat  44308  ssinc  45027  ssdec  45028  uzublem  45380  fmul01  45536  fmul01lt1lem1  45540  limciccioolb  45577  climxrre  45706  ioccncflimc  45841  icocncflimc  45845  cncfiooicclem1  45849  dvnmul  45899  iblspltprt  45929  itgspltprt  45935  stoweidlem20  45976  stoweidlem51  46007  wallispilem3  46023  fourierdlem10  46073  fourierdlem11  46074  fourierdlem14  46077  fourierdlem17  46080  fourierdlem32  46095  fourierdlem33  46096  fourierdlem41  46104  fourierdlem46  46108  fourierdlem48  46110  fourierdlem49  46111  fourierdlem50  46112  fourierdlem73  46135  fourierdlem76  46138  fourierdlem79  46141  fourierdlem93  46155  fourierdlem102  46164  fourierdlem103  46165  fourierdlem104  46166  fourierdlem107  46169  fourierdlem111  46173  fourierdlem114  46176  etransclem23  46213  rrxsnicc  46256  hsphoidmvle2  46541  hsphoidmvle  46542  hoidmv1lelem1  46547  hoidmv1lelem2  46548  hoidmv1lelem3  46549  hoidmvlelem1  46551  hoidifhspdmvle  46576  ovolval4lem2  46606  iinhoiicc  46630  vonicclem2  46640  2leaddle2  47248  bgoldbachlt  47738  logbpw2m1  48417  dignn0ldlem  48452