Theorem leidd 11744

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5107  ℝcr 11067   ≤ cle 11209

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 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-pre-lttri 11142

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214

This theorem is referenced by:  zextle  12607  uzind  12626  uzid  12808  ifle  13157  supxrre  13287  infxrre  13297  nn0fz0  13586  fvinim0ffz  13747  flid  13770  modabs2  13867  monoord  13997  leexp2r  14139  facwordi  14254  faclbnd6  14264  pfxsuffeqwrdeq  14663  repswcshw  14777  iseraltlem2  15649  climcndslem1  15815  cvgrat  15849  eirrlem  16172  ruclem2  16200  ruclem9  16206  sadcaddlem  16427  nn0seqcvgd  16540  eulerthlem2  16752  pcidlem  16843  pc2dvds  16850  pcprmpw2  16853  pcmpt  16863  ramub1lem2  16998  prmolefac  17017  prmgaplem4  17025  pgpfi  19535  zntoslem  21466  psrridm  21872  methaus  24408  nmoid  24630  xrsxmet  24698  reconnlem1  24715  metdstri  24740  nmoleub3  25019  ovolctb  25391  ovolicc1  25417  volcn  25507  mbflimsup  25567  mbfi1fseqlem4  25619  itg2const2  25642  itg2uba  25644  itg2splitlem  25649  itg2cnlem1  25662  itg2cnlem2  25663  iblss  25706  itgless  25718  itgsplitioo  25739  dvge0  25911  dvcvx  25925  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem3  25935  dvfsumrlim  25938  coe1mul4  26005  deg1mul2  26019  ply1divex  26042  deg1submon1p  26058  coe1termlem  26163  dgradd2  26174  dgrco  26181  aaliou3lem2  26251  abelth2  26352  jensen  26899  logexprlim  27136  bcmono  27188  bcmax  27189  dchrisum0flblem1  27419  pntleml  27522  eupth2  30168  blocnilem  30733  wrdt2ind  32875  fiunelros  34164  dstfrvunirn  34466  ballotlemsi  34506  dnibndlem2  36467  knoppndvlem15  36514  relowlssretop  37351  poimirlem28  37642  mblfinlem2  37652  itg2addnclem  37665  itg2gt0cn  37669  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  ssbnd  37782  bfplem1  37816  lcmineqlem4  42020  3lexlogpow5ineq2  42043  intlewftc  42049  aks4d1p1p2  42058  aks4d1p1p4  42059  dvle2  42060  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p1  42064  aks4d1p3  42066  aks4d1p7d1  42070  aks4d1p7  42071  aks4d1p8  42075  aks4d1p9  42076  posbezout  42088  aks6d1c1  42104  aks6d1c2lem4  42115  aks6d1c5lem2  42126  deg1gprod  42128  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  sticksstones22  42156  aks6d1c6lem4  42161  aks6d1c7lem1  42168  aks6d1c7lem2  42169  unitscyglem2  42184  unitscyglem4  42186  fltnlta  42651  acongeq  42972  expdiophlem1  43010  hbt  43119  dvgrat  44301  ssinc  45081  ssdec  45082  uzublem  45426  fmul01  45578  fmul01lt1lem1  45582  limciccioolb  45619  climxrre  45748  ioccncflimc  45883  icocncflimc  45887  cncfiooicclem1  45891  dvnmul  45941  iblspltprt  45971  itgspltprt  45977  stoweidlem20  46018  stoweidlem51  46049  wallispilem3  46065  fourierdlem10  46115  fourierdlem11  46116  fourierdlem14  46119  fourierdlem17  46122  fourierdlem32  46137  fourierdlem33  46138  fourierdlem41  46146  fourierdlem46  46150  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem73  46177  fourierdlem76  46180  fourierdlem79  46183  fourierdlem93  46197  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem107  46211  fourierdlem111  46215  fourierdlem114  46218  etransclem23  46255  rrxsnicc  46298  hsphoidmvle2  46583  hsphoidmvle  46584  hoidmv1lelem1  46589  hoidmv1lelem2  46590  hoidmv1lelem3  46591  hoidmvlelem1  46593  hoidifhspdmvle  46618  ovolval4lem2  46648  iinhoiicc  46672  vonicclem2  46682  2leaddle2  47299  bgoldbachlt  47814  logbpw2m1  48556  dignn0ldlem  48591