Theorem leidd 11863

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  ℝcr 11180   ≤ cle 11325

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-resscn 11238  ax-pre-lttri 11255

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-er 8701  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330

This theorem is used by:  zextle  12753  uzind  12772  uzid  12961  ifle  13308  supxrre  13438  infxrre  13448  nn0fz0  13739  fvinim0ffz  13904  flid  13928  modabs2  14025  monoord  14155  leexp2r  14297  facwordi  14413  faclbnd6  14423  pfxsuffeqwrdeq  14827  repswcshw  14943  iseraltlem2  15830  climcndslem1  15998  cvgrat  16032  eirrlem  16352  ruclem2  16380  ruclem9  16386  sadcaddlem  16607  nn0seqcvgd  16725  eulerthlem2  16939  pcidlem  17030  pc2dvds  17037  pcprmpw2  17040  pcmpt  17050  ramub1lem2  17185  prmolefac  17204  prmgaplem4  17212  pgpfi  19799  zntoslem  21842  psrridm  22250  methaus  24819  nmoid  25041  xrsxmet  25109  reconnlem1  25126  metdstri  25151  nmoleub3  25420  ovolctb  25791  ovolicc1  25817  volcn  25907  mbflimsup  25967  mbfi1fseqlem4  26019  itg2const2  26042  itg2uba  26044  itg2splitlem  26049  itg2cnlem1  26062  itg2cnlem2  26063  iblss  26105  itgless  26117  itgsplitioo  26138  dvge0  26306  dvcvx  26320  dvfsumlem2  26327  dvfsumlem3  26328  dvfsumrlim  26331  coe1mul4  26398  deg1mul2  26412  ply1divex  26435  deg1submon1p  26451  coe1termlem  26557  dgradd2  26567  dgrco  26574  aaliou3lem2  26652  abelth2  26751  jensen  27298  logexprlim  27534  bcmono  27586  bcmax  27587  dchrisum0flblem1  27817  pntleml  27920  eupth2  30822  blocnilem  31388  wrdt2ind  33498  fiunelros  34789  dstfrvunirn  35090  ballotlemsi  35130  dnibndlem2  37315  knoppndvlem15  37362  relowlssretop  38254  poimirlem28  38534  mblfinlem2  38544  itg2addnclem  38557  itg2gt0cn  38561  ftc1anclem7  38585  ftc1anclem8  38586  ftc1anc  38587  ssbnd  38690  bfplem1  38724  lcmineqlem4  43050  3lexlogpow5ineq2  43073  intlewftc  43079  aks4d1p1p2  43088  aks4d1p1p4  43089  dvle2  43090  aks4d1p1p6  43091  aks4d1p1p7  43092  aks4d1p1p5  43093  aks4d1p1  43094  aks4d1p3  43096  aks4d1p7d1  43100  aks4d1p7  43101  aks4d1p8  43105  aks4d1p9  43106  posbezout  43118  aks6d1c1  43134  aks6d1c2lem4  43145  aks6d1c5lem2  43156  deg1gprod  43158  sticksstones10  43173  sticksstones12a  43175  sticksstones12  43176  sticksstones22  43186  aks6d1c6lem4  43191  aks6d1c7lem1  43198  aks6d1c7lem2  43199  unitscyglem2  43214  unitscyglem4  43216  fltnlta  43628  acongeq  43943  expdiophlem1  43981  hbt  44090  dvgrat  45255  ssinc  46045  ssdec  46046  uzublem  46384  fmul01  46536  fmul01lt1lem1  46540  limciccioolb  46577  climxrre  46704  ioccncflimc  46839  icocncflimc  46843  cncfiooicclem1  46847  dvnmul  46897  iblspltprt  46927  itgspltprt  46933  stoweidlem20  46974  stoweidlem51  47005  wallispilem3  47021  fourierdlem10  47071  fourierdlem11  47072  fourierdlem14  47075  fourierdlem17  47078  fourierdlem32  47093  fourierdlem33  47094  fourierdlem41  47102  fourierdlem46  47106  fourierdlem48  47108  fourierdlem49  47109  fourierdlem50  47110  fourierdlem73  47133  fourierdlem76  47136  fourierdlem79  47139  fourierdlem93  47153  fourierdlem102  47162  fourierdlem103  47163  fourierdlem104  47164  fourierdlem107  47167  fourierdlem111  47171  fourierdlem114  47174  etransclem23  47211  rrxsnicc  47254  hsphoidmvle2  47539  hsphoidmvle  47540  hoidmv1lelem1  47545  hoidmv1lelem2  47546  hoidmv1lelem3  47547  hoidmvlelem1  47549  hoidifhspdmvle  47574  ovolval4lem2  47604  iinhoiicc  47628  vonicclem2  47638  2leaddle2  48312  bgoldbachlt  48855  logbpw2m1  49623  dignn0ldlem  49658