Theorem xrleidd

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

	Ref	Expression
Hypothesis	xrleidd.1	$$⊢\phi \to A\in {ℝ}^{*}$$
Assertion	xrleidd	$$⊢\phi \to A\le A$$

Proof

Step	Hyp	Ref	Expression
1		xrleidd.1	$$⊢\phi \to A\in {ℝ}^{*}$$
2		xrleid	$$⊢A\in {ℝ}^{*}\to A\le A$$
3	1 2	syl	$$⊢\phi \to A\le A$$