Theorem xreqle

Description: Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	xreqle	$$⊢\left(A\in {ℝ}^{*}\wedge A=B\right)\to A\le B$$

Proof

Step	Hyp	Ref	Expression
1		xrleid	$$⊢A\in {ℝ}^{*}\to A\le A$$
2	1	adantr	$$⊢\left(A\in {ℝ}^{*}\wedge A=B\right)\to A\le A$$
3		simpr	$$⊢\left(A\in {ℝ}^{*}\wedge A=B\right)\to A=B$$
4		breq2	$$⊢A=B\to \left(A\le A\leftrightarrow A\le B\right)$$
5	4	biimpac	$$⊢\left(A\le A\wedge A=B\right)\to A\le B$$
6	2 3 5	syl2anc	$$⊢\left(A\in {ℝ}^{*}\wedge A=B\right)\to A\le B$$