Theorem leidd 11750

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

Syntax hints:   → wi 4   ∈ wcel 2141   class class class wbr 5099  ℝcr 11069   ≤ cle 11214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pow 5321  ax-pr 5389  ax-un 7714  ax-resscn 11127  ax-pre-lttri 11144

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525  df-er 8673  df-en 8924  df-dom 8925  df-sdom 8926  df-pnf 11215  df-mnf 11216  df-xr 11217  df-ltxr 11218  df-le 11219

This theorem is referenced by:  zextle  12643  uzind  12662  uzid  12851  ifle  13197  supxrre  13327  infxrre  13337  nn0fz0  13627  fvinim0ffz  13792  flid  13815  modabs2  13912  monoord  14042  leexp2r  14184  facwordi  14299  faclbnd6  14309  pfxsuffeqwrdeq  14708  repswcshw  14822  iseraltlem2  15693  climcndslem1  15862  cvgrat  15896  eirrlem  16219  ruclem2  16247  ruclem9  16253  sadcaddlem  16474  nn0seqcvgd  16587  eulerthlem2  16800  pcidlem  16891  pc2dvds  16898  pcprmpw2  16901  pcmpt  16911  ramub1lem2  17046  prmolefac  17065  prmgaplem4  17073  pgpfi  19628  zntoslem  21588  psrridm  21994  methaus  24560  nmoid  24782  xrsxmet  24850  reconnlem1  24867  metdstri  24892  nmoleub3  25161  ovolctb  25532  ovolicc1  25558  volcn  25648  mbflimsup  25708  mbfi1fseqlem4  25760  itg2const2  25783  itg2uba  25785  itg2splitlem  25790  itg2cnlem1  25803  itg2cnlem2  25804  iblss  25847  itgless  25859  itgsplitioo  25880  dvge0  26048  dvcvx  26062  dvfsumlem2  26069  dvfsumlem3  26070  dvfsumrlim  26073  coe1mul4  26140  deg1mul2  26154  ply1divex  26177  deg1submon1p  26193  coe1termlem  26298  dgradd2  26308  dgrco  26315  aaliou3lem2  26384  abelth2  26482  jensen  27030  logexprlim  27266  bcmono  27318  bcmax  27319  dchrisum0flblem1  27549  pntleml  27652  eupth2  30387  blocnilem  30953  wrdt2ind  33092  fiunelros  34432  dstfrvunirn  34733  ballotlemsi  34773  dnibndlem2  36881  knoppndvlem15  36928  relowlssretop  37821  poimirlem28  38111  mblfinlem2  38121  itg2addnclem  38134  itg2gt0cn  38138  ftc1anclem7  38162  ftc1anclem8  38163  ftc1anc  38164  ssbnd  38251  bfplem1  38285  lcmineqlem4  42613  3lexlogpow5ineq2  42636  intlewftc  42642  aks4d1p1p2  42651  aks4d1p1p4  42652  dvle2  42653  aks4d1p1p6  42654  aks4d1p1p7  42655  aks4d1p1p5  42656  aks4d1p1  42657  aks4d1p3  42659  aks4d1p7d1  42663  aks4d1p7  42664  aks4d1p8  42668  aks4d1p9  42669  posbezout  42681  aks6d1c1  42697  aks6d1c2lem4  42708  aks6d1c5lem2  42719  deg1gprod  42721  sticksstones10  42736  sticksstones12a  42738  sticksstones12  42739  sticksstones22  42749  aks6d1c6lem4  42754  aks6d1c7lem1  42761  aks6d1c7lem2  42762  unitscyglem2  42777  unitscyglem4  42779  fltnlta  43209  acongeq  43524  expdiophlem1  43562  hbt  43671  dvgrat  44852  ssinc  45629  ssdec  45630  uzublem  45968  fmul01  46120  fmul01lt1lem1  46124  limciccioolb  46161  climxrre  46288  ioccncflimc  46423  icocncflimc  46427  cncfiooicclem1  46431  dvnmul  46481  iblspltprt  46511  itgspltprt  46517  stoweidlem20  46558  stoweidlem51  46589  wallispilem3  46605  fourierdlem10  46655  fourierdlem11  46656  fourierdlem14  46659  fourierdlem17  46662  fourierdlem32  46677  fourierdlem33  46678  fourierdlem41  46686  fourierdlem46  46690  fourierdlem48  46692  fourierdlem49  46693  fourierdlem50  46694  fourierdlem73  46717  fourierdlem76  46720  fourierdlem79  46723  fourierdlem93  46737  fourierdlem102  46746  fourierdlem103  46747  fourierdlem104  46748  fourierdlem107  46751  fourierdlem111  46755  fourierdlem114  46758  etransclem23  46795  rrxsnicc  46838  hsphoidmvle2  47123  hsphoidmvle  47124  hoidmv1lelem1  47129  hoidmv1lelem2  47130  hoidmv1lelem3  47131  hoidmvlelem1  47133  hoidifhspdmvle  47158  ovolval4lem2  47188  iinhoiicc  47212  vonicclem2  47222  2leaddle2  47856  bgoldbachlt  48399  logbpw2m1  49153  dignn0ldlem  49188