Theorem leidd 11818

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

Syntax hints:   → wi 4   ∈ wcel 2098   class class class wbr 5152  ℝcr 11145   ≤ cle 11287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-resscn 11203  ax-pre-lttri 11220

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-er 8731  df-en 8971  df-dom 8972  df-sdom 8973  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292

This theorem is referenced by:  zextle  12673  uzind  12692  uzid  12875  ifle  13216  supxrre  13346  infxrre  13355  nn0fz0  13639  fvinim0ffz  13791  flid  13813  modabs2  13910  monoord  14037  leexp2r  14178  facwordi  14288  faclbnd6  14298  pfxsuffeqwrdeq  14688  repswcshw  14802  iseraltlem2  15669  climcndslem1  15835  cvgrat  15869  eirrlem  16188  ruclem2  16216  ruclem9  16222  sadcaddlem  16439  nn0seqcvgd  16548  eulerthlem2  16758  pcidlem  16848  pc2dvds  16855  pcprmpw2  16858  pcmpt  16868  ramub1lem2  17003  prmolefac  17022  prmgaplem4  17030  pgpfi  19567  zntoslem  21497  psrridm  21913  methaus  24449  nmoid  24679  xrsxmet  24745  reconnlem1  24762  metdstri  24787  nmoleub3  25066  ovolctb  25439  ovolicc1  25465  volcn  25555  mbflimsup  25615  mbfi1fseqlem4  25668  itg2const2  25691  itg2uba  25693  itg2splitlem  25698  itg2cnlem1  25711  itg2cnlem2  25712  iblss  25754  itgless  25766  itgsplitioo  25787  dvge0  25959  dvcvx  25973  dvfsumlem2  25981  dvfsumlem2OLD  25982  dvfsumlem3  25983  dvfsumrlim  25986  coe1mul4  26056  deg1mul2  26070  ply1divex  26092  deg1submon1p  26108  coe1termlem  26212  dgradd2  26223  dgrco  26230  aaliou3lem2  26298  abelth2  26399  jensen  26941  logexprlim  27178  bcmono  27230  bcmax  27231  dchrisum0flblem1  27461  pntleml  27564  eupth2  30069  blocnilem  30634  wrdt2ind  32695  fiunelros  33826  dstfrvunirn  34127  ballotlemsi  34167  dnibndlem2  35987  knoppndvlem15  36034  relowlssretop  36875  poimirlem28  37154  mblfinlem2  37164  itg2addnclem  37177  itg2gt0cn  37181  ftc1anclem7  37205  ftc1anclem8  37206  ftc1anc  37207  ssbnd  37294  bfplem1  37328  lcmineqlem4  41535  3lexlogpow5ineq2  41558  intlewftc  41564  aks4d1p1p2  41573  aks4d1p1p4  41574  dvle2  41575  aks4d1p1p6  41576  aks4d1p1p7  41577  aks4d1p1p5  41578  aks4d1p1  41579  aks4d1p3  41581  aks4d1p7d1  41585  aks4d1p7  41586  aks4d1p8  41590  aks4d1p9  41591  posbezout  41603  aks6d1c1  41619  aks6d1c2lem4  41630  aks6d1c5lem2  41641  deg1gprod  41644  sticksstones10  41659  sticksstones12a  41661  sticksstones12  41662  sticksstones22  41672  aks6d1c6lem4  41677  aks6d1c7lem1  41684  aks6d1c7lem2  41685  metakunt1  41689  metakunt10  41698  metakunt24  41712  metakunt26  41714  2xp3dxp2ge1d  41725  fltnlta  42118  acongeq  42435  expdiophlem1  42473  hbt  42585  dvgrat  43780  ssinc  44484  ssdec  44485  uzublem  44841  fmul01  44997  fmul01lt1lem1  45001  limciccioolb  45038  climxrre  45167  ioccncflimc  45302  icocncflimc  45306  cncfiooicclem1  45310  dvnmul  45360  iblspltprt  45390  itgspltprt  45396  stoweidlem20  45437  stoweidlem51  45468  wallispilem3  45484  fourierdlem10  45534  fourierdlem11  45535  fourierdlem14  45538  fourierdlem17  45541  fourierdlem32  45556  fourierdlem33  45557  fourierdlem41  45565  fourierdlem46  45569  fourierdlem48  45571  fourierdlem49  45572  fourierdlem50  45573  fourierdlem73  45596  fourierdlem76  45599  fourierdlem79  45602  fourierdlem93  45616  fourierdlem102  45625  fourierdlem103  45626  fourierdlem104  45627  fourierdlem107  45630  fourierdlem111  45634  fourierdlem114  45637  etransclem23  45674  rrxsnicc  45717  hsphoidmvle2  46002  hsphoidmvle  46003  hoidmv1lelem1  46008  hoidmv1lelem2  46009  hoidmv1lelem3  46010  hoidmvlelem1  46012  hoidifhspdmvle  46037  ovolval4lem2  46067  iinhoiicc  46091  vonicclem2  46101  2leaddle2  46707  bgoldbachlt  47182  logbpw2m1  47718  dignn0ldlem  47753