Theorem leidd 11206

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5066  ℝcr 10536   ≤ cle 10676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-resscn 10594  ax-pre-lttri 10611

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681

This theorem is referenced by:  zextle  12056  uzind  12075  uzid  12259  ifle  12591  supxrre  12721  infxrre  12730  nn0fz0  13006  fvinim0ffz  13157  flid  13179  modabs2  13274  monoord  13401  leexp2r  13539  facwordi  13650  faclbnd6  13660  pfxsuffeqwrdeq  14060  repswcshw  14174  iseraltlem2  15039  climcndslem1  15204  cvgrat  15239  eirrlem  15557  ruclem2  15585  ruclem9  15591  sadcaddlem  15806  nn0seqcvgd  15914  eulerthlem2  16119  pcidlem  16208  pc2dvds  16215  pcprmpw2  16218  pcmpt  16228  ramub1lem2  16363  prmolefac  16382  prmgaplem4  16390  pgpfi  18730  psrridm  20184  zntoslem  20703  methaus  23130  nmoid  23351  xrsxmet  23417  reconnlem1  23434  metdstri  23459  nmoleub3  23723  ovolctb  24091  ovolicc1  24117  volcn  24207  mbflimsup  24267  mbfi1fseqlem4  24319  itg2const2  24342  itg2uba  24344  itg2splitlem  24349  itg2cnlem1  24362  itg2cnlem2  24363  iblss  24405  itgless  24417  itgsplitioo  24438  dvge0  24603  dvcvx  24617  dvfsumlem2  24624  dvfsumlem3  24625  dvfsumrlim  24628  coe1mul4  24694  deg1mul2  24708  ply1divex  24730  deg1submon1p  24746  coe1termlem  24848  dgradd2  24858  dgrco  24865  aaliou3lem2  24932  abelth2  25030  jensen  25566  logexprlim  25801  bcmono  25853  bcmax  25854  dchrisum0flblem1  26084  pntleml  26187  eupth2  28018  blocnilem  28581  wrdt2ind  30627  fiunelros  31433  dstfrvunirn  31732  ballotlemsi  31772  dnibndlem2  33818  knoppndvlem15  33865  relowlssretop  34647  poimirlem28  34935  mblfinlem2  34945  itg2addnclem  34958  itg2gt0cn  34962  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  ssbnd  35081  bfplem1  35115  2xp3dxp2ge1d  39146  fltnlta  39324  acongeq  39629  expdiophlem1  39667  hbt  39779  dvgrat  40693  ssinc  41402  ssdec  41403  uzublem  41753  fmul01  41910  fmul01lt1lem1  41914  limciccioolb  41951  climxrre  42080  ioccncflimc  42217  icocncflimc  42221  cncfiooicclem1  42225  dvnmul  42277  iblspltprt  42307  itgspltprt  42313  stoweidlem20  42354  stoweidlem51  42385  wallispilem3  42401  fourierdlem10  42451  fourierdlem11  42452  fourierdlem14  42455  fourierdlem17  42458  fourierdlem32  42473  fourierdlem33  42474  fourierdlem41  42482  fourierdlem46  42486  fourierdlem48  42488  fourierdlem49  42489  fourierdlem50  42490  fourierdlem73  42513  fourierdlem76  42516  fourierdlem79  42519  fourierdlem93  42533  fourierdlem102  42542  fourierdlem103  42543  fourierdlem104  42544  fourierdlem107  42547  fourierdlem111  42551  fourierdlem114  42554  etransclem23  42591  rrxsnicc  42634  hsphoidmvle2  42916  hsphoidmvle  42917  hoidmv1lelem1  42922  hoidmv1lelem2  42923  hoidmv1lelem3  42924  hoidmvlelem1  42926  hoidifhspdmvle  42951  ovolval4lem2  42981  iinhoiicc  43005  vonicclem2  43015  2leaddle2  43547  bgoldbachlt  44027  logbpw2m1  44676  dignn0ldlem  44711