Theorem leidd 11808

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5124  ℝcr 11133   ≤ cle 11275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-resscn 11191  ax-pre-lttri 11208

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280

This theorem is referenced by:  zextle  12671  uzind  12690  uzid  12872  ifle  13218  supxrre  13348  infxrre  13358  nn0fz0  13647  fvinim0ffz  13807  flid  13830  modabs2  13927  monoord  14055  leexp2r  14197  facwordi  14312  faclbnd6  14322  pfxsuffeqwrdeq  14721  repswcshw  14835  iseraltlem2  15704  climcndslem1  15870  cvgrat  15904  eirrlem  16227  ruclem2  16255  ruclem9  16261  sadcaddlem  16481  nn0seqcvgd  16594  eulerthlem2  16806  pcidlem  16897  pc2dvds  16904  pcprmpw2  16907  pcmpt  16917  ramub1lem2  17052  prmolefac  17071  prmgaplem4  17079  pgpfi  19591  zntoslem  21522  psrridm  21928  methaus  24464  nmoid  24686  xrsxmet  24754  reconnlem1  24771  metdstri  24796  nmoleub3  25075  ovolctb  25448  ovolicc1  25474  volcn  25564  mbflimsup  25624  mbfi1fseqlem4  25676  itg2const2  25699  itg2uba  25701  itg2splitlem  25706  itg2cnlem1  25719  itg2cnlem2  25720  iblss  25763  itgless  25775  itgsplitioo  25796  dvge0  25968  dvcvx  25982  dvfsumlem2  25990  dvfsumlem2OLD  25991  dvfsumlem3  25992  dvfsumrlim  25995  coe1mul4  26062  deg1mul2  26076  ply1divex  26099  deg1submon1p  26115  coe1termlem  26220  dgradd2  26231  dgrco  26238  aaliou3lem2  26308  abelth2  26409  jensen  26956  logexprlim  27193  bcmono  27245  bcmax  27246  dchrisum0flblem1  27476  pntleml  27579  eupth2  30225  blocnilem  30790  wrdt2ind  32934  fiunelros  34210  dstfrvunirn  34512  ballotlemsi  34552  dnibndlem2  36502  knoppndvlem15  36549  relowlssretop  37386  poimirlem28  37677  mblfinlem2  37687  itg2addnclem  37700  itg2gt0cn  37704  ftc1anclem7  37728  ftc1anclem8  37729  ftc1anc  37730  ssbnd  37817  bfplem1  37851  lcmineqlem4  42050  3lexlogpow5ineq2  42073  intlewftc  42079  aks4d1p1p2  42088  aks4d1p1p4  42089  dvle2  42090  aks4d1p1p6  42091  aks4d1p1p7  42092  aks4d1p1p5  42093  aks4d1p1  42094  aks4d1p3  42096  aks4d1p7d1  42100  aks4d1p7  42101  aks4d1p8  42105  aks4d1p9  42106  posbezout  42118  aks6d1c1  42134  aks6d1c2lem4  42145  aks6d1c5lem2  42156  deg1gprod  42158  sticksstones10  42173  sticksstones12a  42175  sticksstones12  42176  sticksstones22  42186  aks6d1c6lem4  42191  aks6d1c7lem1  42198  aks6d1c7lem2  42199  unitscyglem2  42214  unitscyglem4  42216  fltnlta  42661  acongeq  42982  expdiophlem1  43020  hbt  43129  dvgrat  44311  ssinc  45091  ssdec  45092  uzublem  45437  fmul01  45589  fmul01lt1lem1  45593  limciccioolb  45630  climxrre  45759  ioccncflimc  45894  icocncflimc  45898  cncfiooicclem1  45902  dvnmul  45952  iblspltprt  45982  itgspltprt  45988  stoweidlem20  46029  stoweidlem51  46060  wallispilem3  46076  fourierdlem10  46126  fourierdlem11  46127  fourierdlem14  46130  fourierdlem17  46133  fourierdlem32  46148  fourierdlem33  46149  fourierdlem41  46157  fourierdlem46  46161  fourierdlem48  46163  fourierdlem49  46164  fourierdlem50  46165  fourierdlem73  46188  fourierdlem76  46191  fourierdlem79  46194  fourierdlem93  46208  fourierdlem102  46217  fourierdlem103  46218  fourierdlem104  46219  fourierdlem107  46222  fourierdlem111  46226  fourierdlem114  46229  etransclem23  46266  rrxsnicc  46309  hsphoidmvle2  46594  hsphoidmvle  46595  hoidmv1lelem1  46600  hoidmv1lelem2  46601  hoidmv1lelem3  46602  hoidmvlelem1  46604  hoidifhspdmvle  46629  ovolval4lem2  46659  iinhoiicc  46683  vonicclem2  46693  2leaddle2  47307  bgoldbachlt  47807  logbpw2m1  48527  dignn0ldlem  48562