Theorem leidd 11909

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   class class class wbr 5106  ℝcr 11226   ≤ cle 11371

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-resscn 11284  ax-pre-lttri 11301

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-er 8745  df-en 9002  df-dom 9003  df-sdom 9004  df-pnf 11372  df-mnf 11373  df-xr 11374  df-ltxr 11375  df-le 11376

This theorem is used by:  zextle  12799  uzind  12818  uzid  13007  ifle  13354  supxrre  13484  infxrre  13494  nn0fz0  13786  fvinim0ffz  13951  flid  13975  modabs2  14072  monoord  14202  leexp2r  14344  facwordi  14460  faclbnd6  14470  pfxsuffeqwrdeq  14875  repswcshw  14991  iseraltlem2  15879  climcndslem1  16047  cvgrat  16081  eirrlem  16401  ruclem2  16429  ruclem9  16435  sadcaddlem  16656  nn0seqcvgd  16774  eulerthlem2  16988  pcidlem  17079  pc2dvds  17086  pcprmpw2  17089  pcmpt  17099  ramub1lem2  17234  prmolefac  17253  prmgaplem4  17261  pgpfi  19849  zntoslem  21892  psrridm  22300  methaus  24869  nmoid  25091  xrsxmet  25159  reconnlem1  25176  metdstri  25201  nmoleub3  25470  ovolctb  25841  ovolicc1  25867  volcn  25957  mbflimsup  26017  mbfi1fseqlem4  26069  itg2const2  26092  itg2uba  26094  itg2splitlem  26099  itg2cnlem1  26112  itg2cnlem2  26113  iblss  26155  itgless  26167  itgsplitioo  26188  dvge0  26356  dvcvx  26370  dvfsumlem2  26377  dvfsumlem3  26378  dvfsumrlim  26381  coe1mul4  26448  deg1mul2  26462  ply1divex  26485  deg1submon1p  26501  coe1termlem  26607  dgradd2  26617  dgrco  26624  aaliou3lem2  26700  abelth2  26799  jensen  27346  logexprlim  27582  bcmono  27634  bcmax  27635  dchrisum0flblem1  27865  pntleml  27968  eupth2  30870  blocnilem  31436  wrdt2ind  33586  fiunelros  34877  dstfrvunirn  35177  ballotlemsi  35217  dnibndlem2  37523  knoppndvlem15  37570  relowlssretop  38478  poimirlem28  38758  mblfinlem2  38768  itg2addnclem  38781  itg2gt0cn  38785  ftc1anclem7  38809  ftc1anclem8  38810  ftc1anc  38811  ssbnd  38914  bfplem1  38948  lcmineqlem4  43274  3lexlogpow5ineq2  43297  intlewftc  43303  aks4d1p1p2  43312  aks4d1p1p4  43313  dvle2  43314  aks4d1p1p6  43315  aks4d1p1p7  43316  aks4d1p1p5  43317  aks4d1p1  43318  aks4d1p3  43320  aks4d1p7d1  43324  aks4d1p7  43325  aks4d1p8  43329  aks4d1p9  43330  posbezout  43342  aks6d1c1  43358  aks6d1c2lem4  43369  aks6d1c5lem2  43380  deg1gprod  43382  sticksstones10  43397  sticksstones12a  43399  sticksstones12  43400  sticksstones22  43410  aks6d1c6lem4  43415  aks6d1c7lem1  43422  aks6d1c7lem2  43423  unitscyglem2  43438  unitscyglem4  43440  fltnlta  43867  acongeq  44183  expdiophlem1  44221  hbt  44324  dvgrat  45488  ssinc  46307  ssdec  46308  uzublem  46645  fmul01  46797  fmul01lt1lem1  46801  limciccioolb  46838  climxrre  46965  ioccncflimc  47100  icocncflimc  47104  cncfiooicclem1  47108  dvnmul  47158  iblspltprt  47188  itgspltprt  47194  stoweidlem20  47235  stoweidlem51  47266  wallispilem3  47282  fourierdlem10  47332  fourierdlem11  47333  fourierdlem14  47336  fourierdlem17  47339  fourierdlem32  47354  fourierdlem33  47355  fourierdlem41  47363  fourierdlem46  47367  fourierdlem48  47369  fourierdlem49  47370  fourierdlem50  47371  fourierdlem73  47394  fourierdlem76  47397  fourierdlem79  47400  fourierdlem93  47414  fourierdlem102  47423  fourierdlem103  47424  fourierdlem104  47425  fourierdlem107  47428  fourierdlem111  47432  fourierdlem114  47435  etransclem23  47472  rrxsnicc  47515  hsphoidmvle2  47800  hsphoidmvle  47801  hoidmv1lelem1  47806  hoidmv1lelem2  47807  hoidmv1lelem3  47808  hoidmvlelem1  47810  hoidifhspdmvle  47835  ovolval4lem2  47865  iinhoiicc  47889  vonicclem2  47899  2leaddle2  48573  bgoldbachlt  49116  logbpw2m1  49884  dignn0ldlem  49919