Theorem leidd 11530

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

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5075  ℝcr 10859   ≤ cle 10999

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7580  ax-resscn 10917  ax-pre-lttri 10934

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-nel 3050  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3433  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5486  df-xp 5592  df-rel 5593  df-cnv 5594  df-co 5595  df-dm 5596  df-rn 5597  df-res 5598  df-ima 5599  df-iota 6386  df-fun 6430  df-fn 6431  df-f 6432  df-f1 6433  df-fo 6434  df-f1o 6435  df-fv 6436  df-er 8487  df-en 8723  df-dom 8724  df-sdom 8725  df-pnf 11000  df-mnf 11001  df-xr 11002  df-ltxr 11003  df-le 11004

This theorem is referenced by:  zextle  12382  uzind  12401  uzid  12586  ifle  12920  supxrre  13050  infxrre  13059  nn0fz0  13343  fvinim0ffz  13495  flid  13517  modabs2  13614  monoord  13742  leexp2r  13881  facwordi  13992  faclbnd6  14002  pfxsuffeqwrdeq  14400  repswcshw  14514  iseraltlem2  15383  climcndslem1  15550  cvgrat  15584  eirrlem  15902  ruclem2  15930  ruclem9  15936  sadcaddlem  16153  nn0seqcvgd  16264  eulerthlem2  16472  pcidlem  16562  pc2dvds  16569  pcprmpw2  16572  pcmpt  16582  ramub1lem2  16717  prmolefac  16736  prmgaplem4  16744  pgpfi  19199  zntoslem  20753  psrridm  21162  methaus  23665  nmoid  23895  xrsxmet  23961  reconnlem1  23978  metdstri  24003  nmoleub3  24271  ovolctb  24643  ovolicc1  24669  volcn  24759  mbflimsup  24819  mbfi1fseqlem4  24872  itg2const2  24895  itg2uba  24897  itg2splitlem  24902  itg2cnlem1  24915  itg2cnlem2  24916  iblss  24958  itgless  24970  itgsplitioo  24991  dvge0  25159  dvcvx  25173  dvfsumlem2  25180  dvfsumlem3  25181  dvfsumrlim  25184  coe1mul4  25254  deg1mul2  25268  ply1divex  25290  deg1submon1p  25306  coe1termlem  25408  dgradd2  25418  dgrco  25425  aaliou3lem2  25492  abelth2  25590  jensen  26127  logexprlim  26362  bcmono  26414  bcmax  26415  dchrisum0flblem1  26645  pntleml  26748  eupth2  28590  blocnilem  29153  wrdt2ind  31212  fiunelros  32129  dstfrvunirn  32428  ballotlemsi  32468  dnibndlem2  34646  knoppndvlem15  34693  relowlssretop  35521  poimirlem28  35792  mblfinlem2  35802  itg2addnclem  35815  itg2gt0cn  35819  ftc1anclem7  35843  ftc1anclem8  35844  ftc1anc  35845  ssbnd  35933  bfplem1  35967  lcmineqlem4  40027  3lexlogpow5ineq2  40050  intlewftc  40056  aks4d1p1p2  40065  aks4d1p1p4  40066  dvle2  40067  aks4d1p1p6  40068  aks4d1p1p7  40069  aks4d1p1p5  40070  aks4d1p1  40071  aks4d1p3  40073  aks4d1p7d1  40077  aks4d1p7  40078  aks4d1p8  40082  aks4d1p9  40083  sticksstones10  40098  sticksstones12a  40100  sticksstones12  40101  sticksstones22  40111  metakunt1  40112  metakunt10  40121  metakunt24  40135  metakunt26  40137  2xp3dxp2ge1d  40149  fltnlta  40487  acongeq  40792  expdiophlem1  40830  hbt  40942  dvgrat  41890  ssinc  42597  ssdec  42598  uzublem  42930  fmul01  43081  fmul01lt1lem1  43085  limciccioolb  43122  climxrre  43251  ioccncflimc  43386  icocncflimc  43390  cncfiooicclem1  43394  dvnmul  43444  iblspltprt  43474  itgspltprt  43480  stoweidlem20  43521  stoweidlem51  43552  wallispilem3  43568  fourierdlem10  43618  fourierdlem11  43619  fourierdlem14  43622  fourierdlem17  43625  fourierdlem32  43640  fourierdlem33  43641  fourierdlem41  43649  fourierdlem46  43653  fourierdlem48  43655  fourierdlem49  43656  fourierdlem50  43657  fourierdlem73  43680  fourierdlem76  43683  fourierdlem79  43686  fourierdlem93  43700  fourierdlem102  43709  fourierdlem103  43710  fourierdlem104  43711  fourierdlem107  43714  fourierdlem111  43718  fourierdlem114  43721  etransclem23  43758  rrxsnicc  43801  hsphoidmvle2  44083  hsphoidmvle  44084  hoidmv1lelem1  44089  hoidmv1lelem2  44090  hoidmv1lelem3  44091  hoidmvlelem1  44093  hoidifhspdmvle  44118  ovolval4lem2  44148  iinhoiicc  44172  vonicclem2  44182  2leaddle2  44747  bgoldbachlt  45222  logbpw2m1  45870  dignn0ldlem  45905