Theorem leidd 11812

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

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5125  ℝcr 11137   ≤ cle 11279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5278  ax-nul 5288  ax-pow 5347  ax-pr 5414  ax-un 7738  ax-resscn 11195  ax-pre-lttri 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3421  df-v 3466  df-sbc 3773  df-csb 3882  df-dif 3936  df-un 3938  df-in 3940  df-ss 3950  df-nul 4316  df-if 4508  df-pw 4584  df-sn 4609  df-pr 4611  df-op 4615  df-uni 4890  df-br 5126  df-opab 5188  df-mpt 5208  df-id 5560  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-iota 6495  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-er 8728  df-en 8969  df-dom 8970  df-sdom 8971  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284

This theorem is referenced by:  zextle  12675  uzind  12694  uzid  12876  ifle  13222  supxrre  13352  infxrre  13361  nn0fz0  13648  fvinim0ffz  13808  flid  13831  modabs2  13928  monoord  14056  leexp2r  14197  facwordi  14311  faclbnd6  14321  pfxsuffeqwrdeq  14719  repswcshw  14833  iseraltlem2  15702  climcndslem1  15868  cvgrat  15902  eirrlem  16223  ruclem2  16251  ruclem9  16257  sadcaddlem  16477  nn0seqcvgd  16590  eulerthlem2  16802  pcidlem  16893  pc2dvds  16900  pcprmpw2  16903  pcmpt  16913  ramub1lem2  17048  prmolefac  17067  prmgaplem4  17075  pgpfi  19596  zntoslem  21542  psrridm  21950  methaus  24496  nmoid  24718  xrsxmet  24786  reconnlem1  24803  metdstri  24828  nmoleub3  25107  ovolctb  25480  ovolicc1  25506  volcn  25596  mbflimsup  25656  mbfi1fseqlem4  25708  itg2const2  25731  itg2uba  25733  itg2splitlem  25738  itg2cnlem1  25751  itg2cnlem2  25752  iblss  25795  itgless  25807  itgsplitioo  25828  dvge0  26000  dvcvx  26014  dvfsumlem2  26022  dvfsumlem2OLD  26023  dvfsumlem3  26024  dvfsumrlim  26027  coe1mul4  26094  deg1mul2  26108  ply1divex  26131  deg1submon1p  26147  coe1termlem  26252  dgradd2  26263  dgrco  26270  aaliou3lem2  26340  abelth2  26441  jensen  26987  logexprlim  27224  bcmono  27276  bcmax  27277  dchrisum0flblem1  27507  pntleml  27610  eupth2  30205  blocnilem  30770  wrdt2ind  32885  fiunelros  34116  dstfrvunirn  34418  ballotlemsi  34458  dnibndlem2  36421  knoppndvlem15  36468  relowlssretop  37305  poimirlem28  37596  mblfinlem2  37606  itg2addnclem  37619  itg2gt0cn  37623  ftc1anclem7  37647  ftc1anclem8  37648  ftc1anc  37649  ssbnd  37736  bfplem1  37770  lcmineqlem4  41974  3lexlogpow5ineq2  41997  intlewftc  42003  aks4d1p1p2  42012  aks4d1p1p4  42013  dvle2  42014  aks4d1p1p6  42015  aks4d1p1p7  42016  aks4d1p1p5  42017  aks4d1p1  42018  aks4d1p3  42020  aks4d1p7d1  42024  aks4d1p7  42025  aks4d1p8  42029  aks4d1p9  42030  posbezout  42042  aks6d1c1  42058  aks6d1c2lem4  42069  aks6d1c5lem2  42080  deg1gprod  42082  sticksstones10  42097  sticksstones12a  42099  sticksstones12  42100  sticksstones22  42110  aks6d1c6lem4  42115  aks6d1c7lem1  42122  aks6d1c7lem2  42123  unitscyglem2  42138  unitscyglem4  42140  metakunt1  42147  metakunt10  42156  metakunt24  42170  metakunt26  42172  2xp3dxp2ge1d  42183  fltnlta  42618  acongeq  42940  expdiophlem1  42978  hbt  43087  dvgrat  44276  ssinc  45037  ssdec  45038  uzublem  45386  fmul01  45540  fmul01lt1lem1  45544  limciccioolb  45581  climxrre  45710  ioccncflimc  45845  icocncflimc  45849  cncfiooicclem1  45853  dvnmul  45903  iblspltprt  45933  itgspltprt  45939  stoweidlem20  45980  stoweidlem51  46011  wallispilem3  46027  fourierdlem10  46077  fourierdlem11  46078  fourierdlem14  46081  fourierdlem17  46084  fourierdlem32  46099  fourierdlem33  46100  fourierdlem41  46108  fourierdlem46  46112  fourierdlem48  46114  fourierdlem49  46115  fourierdlem50  46116  fourierdlem73  46139  fourierdlem76  46142  fourierdlem79  46145  fourierdlem93  46159  fourierdlem102  46168  fourierdlem103  46169  fourierdlem104  46170  fourierdlem107  46173  fourierdlem111  46177  fourierdlem114  46180  etransclem23  46217  rrxsnicc  46260  hsphoidmvle2  46545  hsphoidmvle  46546  hoidmv1lelem1  46551  hoidmv1lelem2  46552  hoidmv1lelem3  46553  hoidmvlelem1  46555  hoidifhspdmvle  46580  ovolval4lem2  46610  iinhoiicc  46634  vonicclem2  46644  2leaddle2  47256  bgoldbachlt  47746  logbpw2m1  48434  dignn0ldlem  48469