Theorem leidd 11195

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

Syntax hints:   → wi 4   ∈ wcel 2111   class class class wbr 5030  ℝcr 10525   ≤ cle 10665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-resscn 10583  ax-pre-lttri 10600

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670

This theorem is referenced by:  zextle  12043  uzind  12062  uzid  12246  ifle  12578  supxrre  12708  infxrre  12717  nn0fz0  13000  fvinim0ffz  13151  flid  13173  modabs2  13268  monoord  13396  leexp2r  13534  facwordi  13645  faclbnd6  13655  pfxsuffeqwrdeq  14051  repswcshw  14165  iseraltlem2  15031  climcndslem1  15196  cvgrat  15231  eirrlem  15549  ruclem2  15577  ruclem9  15583  sadcaddlem  15796  nn0seqcvgd  15904  eulerthlem2  16109  pcidlem  16198  pc2dvds  16205  pcprmpw2  16208  pcmpt  16218  ramub1lem2  16353  prmolefac  16372  prmgaplem4  16380  pgpfi  18722  zntoslem  20248  psrridm  20642  methaus  23127  nmoid  23348  xrsxmet  23414  reconnlem1  23431  metdstri  23456  nmoleub3  23724  ovolctb  24094  ovolicc1  24120  volcn  24210  mbflimsup  24270  mbfi1fseqlem4  24322  itg2const2  24345  itg2uba  24347  itg2splitlem  24352  itg2cnlem1  24365  itg2cnlem2  24366  iblss  24408  itgless  24420  itgsplitioo  24441  dvge0  24609  dvcvx  24623  dvfsumlem2  24630  dvfsumlem3  24631  dvfsumrlim  24634  coe1mul4  24701  deg1mul2  24715  ply1divex  24737  deg1submon1p  24753  coe1termlem  24855  dgradd2  24865  dgrco  24872  aaliou3lem2  24939  abelth2  25037  jensen  25574  logexprlim  25809  bcmono  25861  bcmax  25862  dchrisum0flblem1  26092  pntleml  26195  eupth2  28024  blocnilem  28587  wrdt2ind  30653  fiunelros  31543  dstfrvunirn  31842  ballotlemsi  31882  dnibndlem2  33931  knoppndvlem15  33978  relowlssretop  34780  poimirlem28  35085  mblfinlem2  35095  itg2addnclem  35108  itg2gt0cn  35112  ftc1anclem7  35136  ftc1anclem8  35137  ftc1anc  35138  ssbnd  35226  bfplem1  35260  lcmineqlem4  39320  3lexlogpow5ineq2  39342  intlewftc  39344  metakunt1  39350  metakunt10  39359  metakunt24  39373  metakunt26  39375  2xp3dxp2ge1d  39387  fltnlta  39619  acongeq  39924  expdiophlem1  39962  hbt  40074  dvgrat  41016  ssinc  41723  ssdec  41724  uzublem  42067  fmul01  42222  fmul01lt1lem1  42226  limciccioolb  42263  climxrre  42392  ioccncflimc  42527  icocncflimc  42531  cncfiooicclem1  42535  dvnmul  42585  iblspltprt  42615  itgspltprt  42621  stoweidlem20  42662  stoweidlem51  42693  wallispilem3  42709  fourierdlem10  42759  fourierdlem11  42760  fourierdlem14  42763  fourierdlem17  42766  fourierdlem32  42781  fourierdlem33  42782  fourierdlem41  42790  fourierdlem46  42794  fourierdlem48  42796  fourierdlem49  42797  fourierdlem50  42798  fourierdlem73  42821  fourierdlem76  42824  fourierdlem79  42827  fourierdlem93  42841  fourierdlem102  42850  fourierdlem103  42851  fourierdlem104  42852  fourierdlem107  42855  fourierdlem111  42859  fourierdlem114  42862  etransclem23  42899  rrxsnicc  42942  hsphoidmvle2  43224  hsphoidmvle  43225  hoidmv1lelem1  43230  hoidmv1lelem2  43231  hoidmv1lelem3  43232  hoidmvlelem1  43234  hoidifhspdmvle  43259  ovolval4lem2  43289  iinhoiicc  43313  vonicclem2  43323  2leaddle2  43855  bgoldbachlt  44331  logbpw2m1  44981  dignn0ldlem  45016