Theorem leidd 11471

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5070  ℝcr 10801   ≤ cle 10941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-pre-lttri 10876

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946

This theorem is referenced by:  zextle  12323  uzind  12342  uzid  12526  ifle  12860  supxrre  12990  infxrre  12999  nn0fz0  13283  fvinim0ffz  13434  flid  13456  modabs2  13553  monoord  13681  leexp2r  13820  facwordi  13931  faclbnd6  13941  pfxsuffeqwrdeq  14339  repswcshw  14453  iseraltlem2  15322  climcndslem1  15489  cvgrat  15523  eirrlem  15841  ruclem2  15869  ruclem9  15875  sadcaddlem  16092  nn0seqcvgd  16203  eulerthlem2  16411  pcidlem  16501  pc2dvds  16508  pcprmpw2  16511  pcmpt  16521  ramub1lem2  16656  prmolefac  16675  prmgaplem4  16683  pgpfi  19125  zntoslem  20676  psrridm  21083  methaus  23582  nmoid  23812  xrsxmet  23878  reconnlem1  23895  metdstri  23920  nmoleub3  24188  ovolctb  24559  ovolicc1  24585  volcn  24675  mbflimsup  24735  mbfi1fseqlem4  24788  itg2const2  24811  itg2uba  24813  itg2splitlem  24818  itg2cnlem1  24831  itg2cnlem2  24832  iblss  24874  itgless  24886  itgsplitioo  24907  dvge0  25075  dvcvx  25089  dvfsumlem2  25096  dvfsumlem3  25097  dvfsumrlim  25100  coe1mul4  25170  deg1mul2  25184  ply1divex  25206  deg1submon1p  25222  coe1termlem  25324  dgradd2  25334  dgrco  25341  aaliou3lem2  25408  abelth2  25506  jensen  26043  logexprlim  26278  bcmono  26330  bcmax  26331  dchrisum0flblem1  26561  pntleml  26664  eupth2  28504  blocnilem  29067  wrdt2ind  31127  fiunelros  32042  dstfrvunirn  32341  ballotlemsi  32381  dnibndlem2  34586  knoppndvlem15  34633  relowlssretop  35461  poimirlem28  35732  mblfinlem2  35742  itg2addnclem  35755  itg2gt0cn  35759  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  ssbnd  35873  bfplem1  35907  lcmineqlem4  39968  3lexlogpow5ineq2  39991  intlewftc  39997  aks4d1p1p2  40006  aks4d1p1p4  40007  dvle2  40008  aks4d1p1p6  40009  aks4d1p1p7  40010  aks4d1p1p5  40011  aks4d1p1  40012  aks4d1p3  40014  aks4d1p7d1  40018  aks4d1p7  40019  aks4d1p8  40023  aks4d1p9  40024  sticksstones10  40039  sticksstones12a  40041  sticksstones12  40042  sticksstones22  40052  metakunt1  40053  metakunt10  40062  metakunt24  40076  metakunt26  40078  2xp3dxp2ge1d  40090  fltnlta  40416  acongeq  40721  expdiophlem1  40759  hbt  40871  dvgrat  41819  ssinc  42526  ssdec  42527  uzublem  42860  fmul01  43011  fmul01lt1lem1  43015  limciccioolb  43052  climxrre  43181  ioccncflimc  43316  icocncflimc  43320  cncfiooicclem1  43324  dvnmul  43374  iblspltprt  43404  itgspltprt  43410  stoweidlem20  43451  stoweidlem51  43482  wallispilem3  43498  fourierdlem10  43548  fourierdlem11  43549  fourierdlem14  43552  fourierdlem17  43555  fourierdlem32  43570  fourierdlem33  43571  fourierdlem41  43579  fourierdlem46  43583  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  fourierdlem73  43610  fourierdlem76  43613  fourierdlem79  43616  fourierdlem93  43630  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem107  43644  fourierdlem111  43648  fourierdlem114  43651  etransclem23  43688  rrxsnicc  43731  hsphoidmvle2  44013  hsphoidmvle  44014  hoidmv1lelem1  44019  hoidmv1lelem2  44020  hoidmv1lelem3  44021  hoidmvlelem1  44023  hoidifhspdmvle  44048  ovolval4lem2  44078  iinhoiicc  44102  vonicclem2  44112  2leaddle2  44678  bgoldbachlt  45153  logbpw2m1  45801  dignn0ldlem  45836