Theorem leidd 11707

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5086  ℝcr 11028   ≤ cle 11171

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 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-pre-lttri 11103

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 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176

This theorem is referenced by:  zextle  12593  uzind  12612  uzid  12794  ifle  13140  supxrre  13270  infxrre  13280  nn0fz0  13570  fvinim0ffz  13735  flid  13758  modabs2  13855  monoord  13985  leexp2r  14127  facwordi  14242  faclbnd6  14252  pfxsuffeqwrdeq  14651  repswcshw  14765  iseraltlem2  15636  climcndslem1  15805  cvgrat  15839  eirrlem  16162  ruclem2  16190  ruclem9  16196  sadcaddlem  16417  nn0seqcvgd  16530  eulerthlem2  16743  pcidlem  16834  pc2dvds  16841  pcprmpw2  16844  pcmpt  16854  ramub1lem2  16989  prmolefac  17008  prmgaplem4  17016  pgpfi  19571  zntoslem  21546  psrridm  21951  methaus  24495  nmoid  24717  xrsxmet  24785  reconnlem1  24802  metdstri  24827  nmoleub3  25096  ovolctb  25467  ovolicc1  25493  volcn  25583  mbflimsup  25643  mbfi1fseqlem4  25695  itg2const2  25718  itg2uba  25720  itg2splitlem  25725  itg2cnlem1  25738  itg2cnlem2  25739  iblss  25782  itgless  25794  itgsplitioo  25815  dvge0  25983  dvcvx  25997  dvfsumlem2  26004  dvfsumlem3  26005  dvfsumrlim  26008  coe1mul4  26075  deg1mul2  26089  ply1divex  26112  deg1submon1p  26128  coe1termlem  26233  dgradd2  26243  dgrco  26250  aaliou3lem2  26320  abelth2  26420  jensen  26966  logexprlim  27202  bcmono  27254  bcmax  27255  dchrisum0flblem1  27485  pntleml  27588  eupth2  30324  blocnilem  30890  wrdt2ind  33028  fiunelros  34334  dstfrvunirn  34635  ballotlemsi  34675  dnibndlem2  36755  knoppndvlem15  36802  relowlssretop  37693  poimirlem28  37983  mblfinlem2  37993  itg2addnclem  38006  itg2gt0cn  38010  ftc1anclem7  38034  ftc1anclem8  38035  ftc1anc  38036  ssbnd  38123  bfplem1  38157  lcmineqlem4  42485  3lexlogpow5ineq2  42508  intlewftc  42514  aks4d1p1p2  42523  aks4d1p1p4  42524  dvle2  42525  aks4d1p1p6  42526  aks4d1p1p7  42527  aks4d1p1p5  42528  aks4d1p1  42529  aks4d1p3  42531  aks4d1p7d1  42535  aks4d1p7  42536  aks4d1p8  42540  aks4d1p9  42541  posbezout  42553  aks6d1c1  42569  aks6d1c2lem4  42580  aks6d1c5lem2  42591  deg1gprod  42593  sticksstones10  42608  sticksstones12a  42610  sticksstones12  42611  sticksstones22  42621  aks6d1c6lem4  42626  aks6d1c7lem1  42633  aks6d1c7lem2  42634  unitscyglem2  42649  unitscyglem4  42651  fltnlta  43110  acongeq  43429  expdiophlem1  43467  hbt  43576  dvgrat  44757  ssinc  45535  ssdec  45536  uzublem  45876  fmul01  46028  fmul01lt1lem1  46032  limciccioolb  46069  climxrre  46196  ioccncflimc  46331  icocncflimc  46335  cncfiooicclem1  46339  dvnmul  46389  iblspltprt  46419  itgspltprt  46425  stoweidlem20  46466  stoweidlem51  46497  wallispilem3  46513  fourierdlem10  46563  fourierdlem11  46564  fourierdlem14  46567  fourierdlem17  46570  fourierdlem32  46585  fourierdlem33  46586  fourierdlem41  46594  fourierdlem46  46598  fourierdlem48  46600  fourierdlem49  46601  fourierdlem50  46602  fourierdlem73  46625  fourierdlem76  46628  fourierdlem79  46631  fourierdlem93  46645  fourierdlem102  46654  fourierdlem103  46655  fourierdlem104  46656  fourierdlem107  46659  fourierdlem111  46663  fourierdlem114  46666  etransclem23  46703  rrxsnicc  46746  hsphoidmvle2  47031  hsphoidmvle  47032  hoidmv1lelem1  47037  hoidmv1lelem2  47038  hoidmv1lelem3  47039  hoidmvlelem1  47041  hoidifhspdmvle  47066  ovolval4lem2  47096  iinhoiicc  47120  vonicclem2  47130  2leaddle2  47758  bgoldbachlt  48301  logbpw2m1  49055  dignn0ldlem  49090