Theorem leidd 11715

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5100  ℝcr 11037   ≤ cle 11179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-pre-lttri 11112

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184

This theorem is referenced by:  zextle  12577  uzind  12596  uzid  12778  ifle  13124  supxrre  13254  infxrre  13264  nn0fz0  13553  fvinim0ffz  13717  flid  13740  modabs2  13837  monoord  13967  leexp2r  14109  facwordi  14224  faclbnd6  14234  pfxsuffeqwrdeq  14633  repswcshw  14747  iseraltlem2  15618  climcndslem1  15784  cvgrat  15818  eirrlem  16141  ruclem2  16169  ruclem9  16175  sadcaddlem  16396  nn0seqcvgd  16509  eulerthlem2  16721  pcidlem  16812  pc2dvds  16819  pcprmpw2  16822  pcmpt  16832  ramub1lem2  16967  prmolefac  16986  prmgaplem4  16994  pgpfi  19546  zntoslem  21523  psrridm  21930  methaus  24476  nmoid  24698  xrsxmet  24766  reconnlem1  24783  metdstri  24808  nmoleub3  25087  ovolctb  25459  ovolicc1  25485  volcn  25575  mbflimsup  25635  mbfi1fseqlem4  25687  itg2const2  25710  itg2uba  25712  itg2splitlem  25717  itg2cnlem1  25730  itg2cnlem2  25731  iblss  25774  itgless  25786  itgsplitioo  25807  dvge0  25979  dvcvx  25993  dvfsumlem2  26001  dvfsumlem2OLD  26002  dvfsumlem3  26003  dvfsumrlim  26006  coe1mul4  26073  deg1mul2  26087  ply1divex  26110  deg1submon1p  26126  coe1termlem  26231  dgradd2  26242  dgrco  26249  aaliou3lem2  26319  abelth2  26420  jensen  26967  logexprlim  27204  bcmono  27256  bcmax  27257  dchrisum0flblem1  27487  pntleml  27590  eupth2  30326  blocnilem  30891  wrdt2ind  33045  fiunelros  34351  dstfrvunirn  34652  ballotlemsi  34692  dnibndlem2  36698  knoppndvlem15  36745  relowlssretop  37612  poimirlem28  37893  mblfinlem2  37903  itg2addnclem  37916  itg2gt0cn  37920  ftc1anclem7  37944  ftc1anclem8  37945  ftc1anc  37946  ssbnd  38033  bfplem1  38067  lcmineqlem4  42396  3lexlogpow5ineq2  42419  intlewftc  42425  aks4d1p1p2  42434  aks4d1p1p4  42435  dvle2  42436  aks4d1p1p6  42437  aks4d1p1p7  42438  aks4d1p1p5  42439  aks4d1p1  42440  aks4d1p3  42442  aks4d1p7d1  42446  aks4d1p7  42447  aks4d1p8  42451  aks4d1p9  42452  posbezout  42464  aks6d1c1  42480  aks6d1c2lem4  42491  aks6d1c5lem2  42502  deg1gprod  42504  sticksstones10  42519  sticksstones12a  42521  sticksstones12  42522  sticksstones22  42532  aks6d1c6lem4  42537  aks6d1c7lem1  42544  aks6d1c7lem2  42545  unitscyglem2  42560  unitscyglem4  42562  fltnlta  43015  acongeq  43334  expdiophlem1  43372  hbt  43481  dvgrat  44662  ssinc  45440  ssdec  45441  uzublem  45782  fmul01  45934  fmul01lt1lem1  45938  limciccioolb  45975  climxrre  46102  ioccncflimc  46237  icocncflimc  46241  cncfiooicclem1  46245  dvnmul  46295  iblspltprt  46325  itgspltprt  46331  stoweidlem20  46372  stoweidlem51  46403  wallispilem3  46419  fourierdlem10  46469  fourierdlem11  46470  fourierdlem14  46473  fourierdlem17  46476  fourierdlem32  46491  fourierdlem33  46492  fourierdlem41  46500  fourierdlem46  46504  fourierdlem48  46506  fourierdlem49  46507  fourierdlem50  46508  fourierdlem73  46531  fourierdlem76  46534  fourierdlem79  46537  fourierdlem93  46551  fourierdlem102  46560  fourierdlem103  46561  fourierdlem104  46562  fourierdlem107  46565  fourierdlem111  46569  fourierdlem114  46572  etransclem23  46609  rrxsnicc  46652  hsphoidmvle2  46937  hsphoidmvle  46938  hoidmv1lelem1  46943  hoidmv1lelem2  46944  hoidmv1lelem3  46945  hoidmvlelem1  46947  hoidifhspdmvle  46972  ovolval4lem2  47002  iinhoiicc  47026  vonicclem2  47036  2leaddle2  47652  bgoldbachlt  48167  logbpw2m1  48921  dignn0ldlem  48956