Theorem leidd 11714

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

Syntax hints:   → wi 4   ∈ wcel 2119   class class class wbr 5079  ℝcr 11035   ≤ cle 11178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-resscn 11093  ax-pre-lttri 11110

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-xr 11181  df-ltxr 11182  df-le 11183

This theorem is referenced by:  zextle  12600  uzind  12619  uzid  12801  ifle  13147  supxrre  13277  infxrre  13287  nn0fz0  13577  fvinim0ffz  13742  flid  13765  modabs2  13862  monoord  13992  leexp2r  14134  facwordi  14249  faclbnd6  14259  pfxsuffeqwrdeq  14658  repswcshw  14772  iseraltlem2  15643  climcndslem1  15812  cvgrat  15846  eirrlem  16169  ruclem2  16197  ruclem9  16203  sadcaddlem  16424  nn0seqcvgd  16537  eulerthlem2  16750  pcidlem  16841  pc2dvds  16848  pcprmpw2  16851  pcmpt  16861  ramub1lem2  16996  prmolefac  17015  prmgaplem4  17023  pgpfi  19578  zntoslem  21538  psrridm  21944  methaus  24510  nmoid  24732  xrsxmet  24800  reconnlem1  24817  metdstri  24842  nmoleub3  25111  ovolctb  25482  ovolicc1  25508  volcn  25598  mbflimsup  25658  mbfi1fseqlem4  25710  itg2const2  25733  itg2uba  25735  itg2splitlem  25740  itg2cnlem1  25753  itg2cnlem2  25754  iblss  25797  itgless  25809  itgsplitioo  25830  dvge0  25998  dvcvx  26012  dvfsumlem2  26019  dvfsumlem3  26020  dvfsumrlim  26023  coe1mul4  26090  deg1mul2  26104  ply1divex  26127  deg1submon1p  26143  coe1termlem  26248  dgradd2  26258  dgrco  26265  aaliou3lem2  26334  abelth2  26432  jensen  26977  logexprlim  27213  bcmono  27265  bcmax  27266  dchrisum0flblem1  27496  pntleml  27599  eupth2  30334  blocnilem  30900  wrdt2ind  33039  fiunelros  34365  dstfrvunirn  34666  ballotlemsi  34706  dnibndlem2  36792  knoppndvlem15  36839  relowlssretop  37732  poimirlem28  38022  mblfinlem2  38032  itg2addnclem  38045  itg2gt0cn  38049  ftc1anclem7  38073  ftc1anclem8  38074  ftc1anc  38075  ssbnd  38162  bfplem1  38196  lcmineqlem4  42524  3lexlogpow5ineq2  42547  intlewftc  42553  aks4d1p1p2  42562  aks4d1p1p4  42563  dvle2  42564  aks4d1p1p6  42565  aks4d1p1p7  42566  aks4d1p1p5  42567  aks4d1p1  42568  aks4d1p3  42570  aks4d1p7d1  42574  aks4d1p7  42575  aks4d1p8  42579  aks4d1p9  42580  posbezout  42592  aks6d1c1  42608  aks6d1c2lem4  42619  aks6d1c5lem2  42630  deg1gprod  42632  sticksstones10  42647  sticksstones12a  42649  sticksstones12  42650  sticksstones22  42660  aks6d1c6lem4  42665  aks6d1c7lem1  42672  aks6d1c7lem2  42673  unitscyglem2  42688  unitscyglem4  42690  fltnlta  43120  acongeq  43435  expdiophlem1  43473  hbt  43582  dvgrat  44763  ssinc  45541  ssdec  45542  uzublem  45880  fmul01  46032  fmul01lt1lem1  46036  limciccioolb  46073  climxrre  46200  ioccncflimc  46335  icocncflimc  46339  cncfiooicclem1  46343  dvnmul  46393  iblspltprt  46423  itgspltprt  46429  stoweidlem20  46470  stoweidlem51  46501  wallispilem3  46517  fourierdlem10  46567  fourierdlem11  46568  fourierdlem14  46571  fourierdlem17  46574  fourierdlem32  46589  fourierdlem33  46590  fourierdlem41  46598  fourierdlem46  46602  fourierdlem48  46604  fourierdlem49  46605  fourierdlem50  46606  fourierdlem73  46629  fourierdlem76  46632  fourierdlem79  46635  fourierdlem93  46649  fourierdlem102  46658  fourierdlem103  46659  fourierdlem104  46660  fourierdlem107  46663  fourierdlem111  46667  fourierdlem114  46670  etransclem23  46707  rrxsnicc  46750  hsphoidmvle2  47035  hsphoidmvle  47036  hoidmv1lelem1  47041  hoidmv1lelem2  47042  hoidmv1lelem3  47043  hoidmvlelem1  47045  hoidifhspdmvle  47070  ovolval4lem2  47100  iinhoiicc  47124  vonicclem2  47134  2leaddle2  47768  bgoldbachlt  48311  logbpw2m1  49065  dignn0ldlem  49100