Theorem xrleidd 12831

Description: 'Less than or equal to' is reflexive for extended reals. Deduction form of xrleid 12830. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypothesis

Ref	Expression
xrleidd.1	⊢ (𝜑 → 𝐴 ∈ ℝ*)

Assertion

Ref	Expression
xrleidd	⊢ (𝜑 → 𝐴 ≤ 𝐴)

Proof of Theorem xrleidd

Step	Hyp	Ref	Expression
1		xrleidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
2		xrleid 12830	. 2 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ≤ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5075  ℝ^*cxr 10955   ≤ cle 10957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7571  ax-cnex 10874  ax-resscn 10875  ax-pre-lttri 10892  ax-pre-lttrn 10893

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3429  df-sbc 3717  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5485  df-po 5499  df-so 5500  df-xp 5591  df-rel 5592  df-cnv 5593  df-co 5594  df-dm 5595  df-rn 5596  df-res 5597  df-ima 5598  df-iota 6381  df-fun 6425  df-fn 6426  df-f 6427  df-f1 6428  df-fo 6429  df-f1o 6430  df-fv 6431  df-er 8461  df-en 8697  df-dom 8698  df-sdom 8699  df-pnf 10958  df-mnf 10959  df-xr 10960  df-ltxr 10961  df-le 10962

This theorem is referenced by:  xleadd1a  12932  supxrre  13006  infxrre  13015  ioounsn  13154  snunioo  13155  snunico  13156  limsupgre  15134  limsupbnd1  15135  limsupbnd2  15136  pcdvdstr  16521  pcadd  16534  imasdsf1olem  23470  blssps  23521  blss  23522  blcld  23605  nmolb  23825  metds0  23957  metdstri  23958  metdseq0  23961  itg2eqa  24853  mdeglt  25173  deg1lt  25205  eliccelico  31040  elicoelioo  31041  difioo  31045  xrge0omnd  31279  esumpmono  31989  signsply0  32472  iocinico  41001  xadd0ge  42791  infxrpnf  42918  monoordxrv  42954  iooiinioc  43026  icossico2  43034  limcresiooub  43115  liminflelimsupuz  43258  ismbl4  43466  sge0prle  43871  iunhoiioo  44146  iccpartleu  44810  iccpartgel  44811  iccdisj2  46121