Theorem leidd 11768

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

Syntax hints:   → wi 4   ∈ wcel 2145   class class class wbr 5105  ℝcr 11087   ≤ cle 11232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-resscn 11145  ax-pre-lttri 11162

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237

This theorem is referenced by:  zextle  12660  uzind  12679  uzid  12868  ifle  13214  supxrre  13344  infxrre  13354  nn0fz0  13644  fvinim0ffz  13809  flid  13832  modabs2  13929  monoord  14059  leexp2r  14201  facwordi  14316  faclbnd6  14326  pfxsuffeqwrdeq  14725  repswcshw  14839  iseraltlem2  15724  climcndslem1  15893  cvgrat  15927  eirrlem  16250  ruclem2  16278  ruclem9  16284  sadcaddlem  16505  nn0seqcvgd  16618  eulerthlem2  16831  pcidlem  16922  pc2dvds  16929  pcprmpw2  16932  pcmpt  16942  ramub1lem2  17077  prmolefac  17096  prmgaplem4  17104  pgpfi  19666  zntoslem  21666  psrridm  22072  methaus  24638  nmoid  24860  xrsxmet  24928  reconnlem1  24945  metdstri  24970  nmoleub3  25239  ovolctb  25610  ovolicc1  25636  volcn  25726  mbflimsup  25786  mbfi1fseqlem4  25838  itg2const2  25861  itg2uba  25863  itg2splitlem  25868  itg2cnlem1  25881  itg2cnlem2  25882  iblss  25925  itgless  25937  itgsplitioo  25958  dvge0  26126  dvcvx  26140  dvfsumlem2  26147  dvfsumlem3  26148  dvfsumrlim  26151  coe1mul4  26218  deg1mul2  26232  ply1divex  26255  deg1submon1p  26271  coe1termlem  26376  dgradd2  26386  dgrco  26393  aaliou3lem2  26465  abelth2  26563  jensen  27111  logexprlim  27347  bcmono  27399  bcmax  27400  dchrisum0flblem1  27630  pntleml  27733  eupth2  30499  blocnilem  31065  wrdt2ind  33186  fiunelros  34481  dstfrvunirn  34782  ballotlemsi  34822  dnibndlem2  36930  knoppndvlem15  36977  relowlssretop  37869  poimirlem28  38159  mblfinlem2  38169  itg2addnclem  38182  itg2gt0cn  38186  ftc1anclem7  38210  ftc1anclem8  38211  ftc1anc  38212  ssbnd  38299  bfplem1  38333  lcmineqlem4  42661  3lexlogpow5ineq2  42684  intlewftc  42690  aks4d1p1p2  42699  aks4d1p1p4  42700  dvle2  42701  aks4d1p1p6  42702  aks4d1p1p7  42703  aks4d1p1p5  42704  aks4d1p1  42705  aks4d1p3  42707  aks4d1p7d1  42711  aks4d1p7  42712  aks4d1p8  42716  aks4d1p9  42717  posbezout  42729  aks6d1c1  42745  aks6d1c2lem4  42756  aks6d1c5lem2  42767  deg1gprod  42769  sticksstones10  42784  sticksstones12a  42786  sticksstones12  42787  sticksstones22  42797  aks6d1c6lem4  42802  aks6d1c7lem1  42809  aks6d1c7lem2  42810  unitscyglem2  42825  unitscyglem4  42827  fltnlta  43257  acongeq  43572  expdiophlem1  43610  hbt  43719  dvgrat  44886  ssinc  45663  ssdec  45664  uzublem  46002  fmul01  46154  fmul01lt1lem1  46158  limciccioolb  46195  climxrre  46322  ioccncflimc  46457  icocncflimc  46461  cncfiooicclem1  46465  dvnmul  46515  iblspltprt  46545  itgspltprt  46551  stoweidlem20  46592  stoweidlem51  46623  wallispilem3  46639  fourierdlem10  46689  fourierdlem11  46690  fourierdlem14  46693  fourierdlem17  46696  fourierdlem32  46711  fourierdlem33  46712  fourierdlem41  46720  fourierdlem46  46724  fourierdlem48  46726  fourierdlem49  46727  fourierdlem50  46728  fourierdlem73  46751  fourierdlem76  46754  fourierdlem79  46757  fourierdlem93  46771  fourierdlem102  46780  fourierdlem103  46781  fourierdlem104  46782  fourierdlem107  46785  fourierdlem111  46789  fourierdlem114  46792  etransclem23  46829  rrxsnicc  46872  hsphoidmvle2  47157  hsphoidmvle  47158  hoidmv1lelem1  47163  hoidmv1lelem2  47164  hoidmv1lelem3  47165  hoidmvlelem1  47167  hoidifhspdmvle  47192  ovolval4lem2  47222  iinhoiicc  47246  vonicclem2  47256  2leaddle2  47890  bgoldbachlt  48433  logbpw2m1  49198  dignn0ldlem  49233