Theorem leidd 11856

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5166  ℝcr 11183   ≤ cle 11325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-resscn 11241  ax-pre-lttri 11258

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330

This theorem is referenced by:  zextle  12716  uzind  12735  uzid  12918  ifle  13259  supxrre  13389  infxrre  13398  nn0fz0  13682  fvinim0ffz  13836  flid  13859  modabs2  13956  monoord  14083  leexp2r  14224  facwordi  14338  faclbnd6  14348  pfxsuffeqwrdeq  14746  repswcshw  14860  iseraltlem2  15731  climcndslem1  15897  cvgrat  15931  eirrlem  16252  ruclem2  16280  ruclem9  16286  sadcaddlem  16503  nn0seqcvgd  16617  eulerthlem2  16829  pcidlem  16919  pc2dvds  16926  pcprmpw2  16929  pcmpt  16939  ramub1lem2  17074  prmolefac  17093  prmgaplem4  17101  pgpfi  19647  zntoslem  21598  psrridm  22006  methaus  24554  nmoid  24784  xrsxmet  24850  reconnlem1  24867  metdstri  24892  nmoleub3  25171  ovolctb  25544  ovolicc1  25570  volcn  25660  mbflimsup  25720  mbfi1fseqlem4  25773  itg2const2  25796  itg2uba  25798  itg2splitlem  25803  itg2cnlem1  25816  itg2cnlem2  25817  iblss  25860  itgless  25872  itgsplitioo  25893  dvge0  26065  dvcvx  26079  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumlem3  26089  dvfsumrlim  26092  coe1mul4  26159  deg1mul2  26173  ply1divex  26196  deg1submon1p  26212  coe1termlem  26317  dgradd2  26328  dgrco  26335  aaliou3lem2  26403  abelth2  26504  jensen  27050  logexprlim  27287  bcmono  27339  bcmax  27340  dchrisum0flblem1  27570  pntleml  27673  eupth2  30271  blocnilem  30836  wrdt2ind  32920  fiunelros  34138  dstfrvunirn  34439  ballotlemsi  34479  dnibndlem2  36445  knoppndvlem15  36492  relowlssretop  37329  poimirlem28  37608  mblfinlem2  37618  itg2addnclem  37631  itg2gt0cn  37635  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  ssbnd  37748  bfplem1  37782  lcmineqlem4  41989  3lexlogpow5ineq2  42012  intlewftc  42018  aks4d1p1p2  42027  aks4d1p1p4  42028  dvle2  42029  aks4d1p1p6  42030  aks4d1p1p7  42031  aks4d1p1p5  42032  aks4d1p1  42033  aks4d1p3  42035  aks4d1p7d1  42039  aks4d1p7  42040  aks4d1p8  42044  aks4d1p9  42045  posbezout  42057  aks6d1c1  42073  aks6d1c2lem4  42084  aks6d1c5lem2  42095  deg1gprod  42097  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  sticksstones22  42125  aks6d1c6lem4  42130  aks6d1c7lem1  42137  aks6d1c7lem2  42138  unitscyglem2  42153  unitscyglem4  42155  metakunt1  42162  metakunt10  42171  metakunt24  42185  metakunt26  42187  2xp3dxp2ge1d  42198  fltnlta  42618  acongeq  42940  expdiophlem1  42978  hbt  43087  dvgrat  44281  ssinc  44989  ssdec  44990  uzublem  45345  fmul01  45501  fmul01lt1lem1  45505  limciccioolb  45542  climxrre  45671  ioccncflimc  45806  icocncflimc  45810  cncfiooicclem1  45814  dvnmul  45864  iblspltprt  45894  itgspltprt  45900  stoweidlem20  45941  stoweidlem51  45972  wallispilem3  45988  fourierdlem10  46038  fourierdlem11  46039  fourierdlem14  46042  fourierdlem17  46045  fourierdlem32  46060  fourierdlem33  46061  fourierdlem41  46069  fourierdlem46  46073  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem73  46100  fourierdlem76  46103  fourierdlem79  46106  fourierdlem93  46120  fourierdlem102  46129  fourierdlem103  46130  fourierdlem104  46131  fourierdlem107  46134  fourierdlem111  46138  fourierdlem114  46141  etransclem23  46178  rrxsnicc  46221  hsphoidmvle2  46506  hsphoidmvle  46507  hoidmv1lelem1  46512  hoidmv1lelem2  46513  hoidmv1lelem3  46514  hoidmvlelem1  46516  hoidifhspdmvle  46541  ovolval4lem2  46571  iinhoiicc  46595  vonicclem2  46605  2leaddle2  47213  bgoldbachlt  47687  logbpw2m1  48301  dignn0ldlem  48336