Theorem leidd 11550

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

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5075  ℝcr 10879   ≤ cle 11019

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-resscn 10937  ax-pre-lttri 10954

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 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-nel 3051  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024

This theorem is referenced by:  zextle  12402  uzind  12421  uzid  12606  ifle  12940  supxrre  13070  infxrre  13079  nn0fz0  13363  fvinim0ffz  13515  flid  13537  modabs2  13634  monoord  13762  leexp2r  13901  facwordi  14012  faclbnd6  14022  pfxsuffeqwrdeq  14420  repswcshw  14534  iseraltlem2  15403  climcndslem1  15570  cvgrat  15604  eirrlem  15922  ruclem2  15950  ruclem9  15956  sadcaddlem  16173  nn0seqcvgd  16284  eulerthlem2  16492  pcidlem  16582  pc2dvds  16589  pcprmpw2  16592  pcmpt  16602  ramub1lem2  16737  prmolefac  16756  prmgaplem4  16764  pgpfi  19219  zntoslem  20773  psrridm  21182  methaus  23685  nmoid  23915  xrsxmet  23981  reconnlem1  23998  metdstri  24023  nmoleub3  24291  ovolctb  24663  ovolicc1  24689  volcn  24779  mbflimsup  24839  mbfi1fseqlem4  24892  itg2const2  24915  itg2uba  24917  itg2splitlem  24922  itg2cnlem1  24935  itg2cnlem2  24936  iblss  24978  itgless  24990  itgsplitioo  25011  dvge0  25179  dvcvx  25193  dvfsumlem2  25200  dvfsumlem3  25201  dvfsumrlim  25204  coe1mul4  25274  deg1mul2  25288  ply1divex  25310  deg1submon1p  25326  coe1termlem  25428  dgradd2  25438  dgrco  25445  aaliou3lem2  25512  abelth2  25610  jensen  26147  logexprlim  26382  bcmono  26434  bcmax  26435  dchrisum0flblem1  26665  pntleml  26768  eupth2  28612  blocnilem  29175  wrdt2ind  31234  fiunelros  32151  dstfrvunirn  32450  ballotlemsi  32490  dnibndlem2  34668  knoppndvlem15  34715  relowlssretop  35543  poimirlem28  35814  mblfinlem2  35824  itg2addnclem  35837  itg2gt0cn  35841  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  ssbnd  35955  bfplem1  35989  lcmineqlem4  40047  3lexlogpow5ineq2  40070  intlewftc  40076  aks4d1p1p2  40085  aks4d1p1p4  40086  dvle2  40087  aks4d1p1p6  40088  aks4d1p1p7  40089  aks4d1p1p5  40090  aks4d1p1  40091  aks4d1p3  40093  aks4d1p7d1  40097  aks4d1p7  40098  aks4d1p8  40102  aks4d1p9  40103  sticksstones10  40118  sticksstones12a  40120  sticksstones12  40121  sticksstones22  40131  metakunt1  40132  metakunt10  40141  metakunt24  40155  metakunt26  40157  2xp3dxp2ge1d  40169  fltnlta  40507  acongeq  40812  expdiophlem1  40850  hbt  40962  dvgrat  41937  ssinc  42644  ssdec  42645  uzublem  42977  fmul01  43128  fmul01lt1lem1  43132  limciccioolb  43169  climxrre  43298  ioccncflimc  43433  icocncflimc  43437  cncfiooicclem1  43441  dvnmul  43491  iblspltprt  43521  itgspltprt  43527  stoweidlem20  43568  stoweidlem51  43599  wallispilem3  43615  fourierdlem10  43665  fourierdlem11  43666  fourierdlem14  43669  fourierdlem17  43672  fourierdlem32  43687  fourierdlem33  43688  fourierdlem41  43696  fourierdlem46  43700  fourierdlem48  43702  fourierdlem49  43703  fourierdlem50  43704  fourierdlem73  43727  fourierdlem76  43730  fourierdlem79  43733  fourierdlem93  43747  fourierdlem102  43756  fourierdlem103  43757  fourierdlem104  43758  fourierdlem107  43761  fourierdlem111  43765  fourierdlem114  43768  etransclem23  43805  rrxsnicc  43848  hsphoidmvle2  44130  hsphoidmvle  44131  hoidmv1lelem1  44136  hoidmv1lelem2  44137  hoidmv1lelem3  44138  hoidmvlelem1  44140  hoidifhspdmvle  44165  ovolval4lem2  44195  iinhoiicc  44219  vonicclem2  44229  2leaddle2  44801  bgoldbachlt  45276  logbpw2m1  45924  dignn0ldlem  45959