Theorem leidd 11751

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5110  ℝcr 11074   ≤ cle 11216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-pre-lttri 11149

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221

This theorem is referenced by:  zextle  12614  uzind  12633  uzid  12815  ifle  13164  supxrre  13294  infxrre  13304  nn0fz0  13593  fvinim0ffz  13754  flid  13777  modabs2  13874  monoord  14004  leexp2r  14146  facwordi  14261  faclbnd6  14271  pfxsuffeqwrdeq  14670  repswcshw  14784  iseraltlem2  15656  climcndslem1  15822  cvgrat  15856  eirrlem  16179  ruclem2  16207  ruclem9  16213  sadcaddlem  16434  nn0seqcvgd  16547  eulerthlem2  16759  pcidlem  16850  pc2dvds  16857  pcprmpw2  16860  pcmpt  16870  ramub1lem2  17005  prmolefac  17024  prmgaplem4  17032  pgpfi  19542  zntoslem  21473  psrridm  21879  methaus  24415  nmoid  24637  xrsxmet  24705  reconnlem1  24722  metdstri  24747  nmoleub3  25026  ovolctb  25398  ovolicc1  25424  volcn  25514  mbflimsup  25574  mbfi1fseqlem4  25626  itg2const2  25649  itg2uba  25651  itg2splitlem  25656  itg2cnlem1  25669  itg2cnlem2  25670  iblss  25713  itgless  25725  itgsplitioo  25746  dvge0  25918  dvcvx  25932  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumlem3  25942  dvfsumrlim  25945  coe1mul4  26012  deg1mul2  26026  ply1divex  26049  deg1submon1p  26065  coe1termlem  26170  dgradd2  26181  dgrco  26188  aaliou3lem2  26258  abelth2  26359  jensen  26906  logexprlim  27143  bcmono  27195  bcmax  27196  dchrisum0flblem1  27426  pntleml  27529  eupth2  30175  blocnilem  30740  wrdt2ind  32882  fiunelros  34171  dstfrvunirn  34473  ballotlemsi  34513  dnibndlem2  36474  knoppndvlem15  36521  relowlssretop  37358  poimirlem28  37649  mblfinlem2  37659  itg2addnclem  37672  itg2gt0cn  37676  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  ssbnd  37789  bfplem1  37823  lcmineqlem4  42027  3lexlogpow5ineq2  42050  intlewftc  42056  aks4d1p1p2  42065  aks4d1p1p4  42066  dvle2  42067  aks4d1p1p6  42068  aks4d1p1p7  42069  aks4d1p1p5  42070  aks4d1p1  42071  aks4d1p3  42073  aks4d1p7d1  42077  aks4d1p7  42078  aks4d1p8  42082  aks4d1p9  42083  posbezout  42095  aks6d1c1  42111  aks6d1c2lem4  42122  aks6d1c5lem2  42133  deg1gprod  42135  sticksstones10  42150  sticksstones12a  42152  sticksstones12  42153  sticksstones22  42163  aks6d1c6lem4  42168  aks6d1c7lem1  42175  aks6d1c7lem2  42176  unitscyglem2  42191  unitscyglem4  42193  fltnlta  42658  acongeq  42979  expdiophlem1  43017  hbt  43126  dvgrat  44308  ssinc  45088  ssdec  45089  uzublem  45433  fmul01  45585  fmul01lt1lem1  45589  limciccioolb  45626  climxrre  45755  ioccncflimc  45890  icocncflimc  45894  cncfiooicclem1  45898  dvnmul  45948  iblspltprt  45978  itgspltprt  45984  stoweidlem20  46025  stoweidlem51  46056  wallispilem3  46072  fourierdlem10  46122  fourierdlem11  46123  fourierdlem14  46126  fourierdlem17  46129  fourierdlem32  46144  fourierdlem33  46145  fourierdlem41  46153  fourierdlem46  46157  fourierdlem48  46159  fourierdlem49  46160  fourierdlem50  46161  fourierdlem73  46184  fourierdlem76  46187  fourierdlem79  46190  fourierdlem93  46204  fourierdlem102  46213  fourierdlem103  46214  fourierdlem104  46215  fourierdlem107  46218  fourierdlem111  46222  fourierdlem114  46225  etransclem23  46262  rrxsnicc  46305  hsphoidmvle2  46590  hsphoidmvle  46591  hoidmv1lelem1  46596  hoidmv1lelem2  46597  hoidmv1lelem3  46598  hoidmvlelem1  46600  hoidifhspdmvle  46625  ovolval4lem2  46655  iinhoiicc  46679  vonicclem2  46689  2leaddle2  47303  bgoldbachlt  47818  logbpw2m1  48560  dignn0ldlem  48595