Theorem eqle

Description: Equality implies 'less than or equal to'. (Contributed by NM, 4-Apr-2005)

	Ref	Expression
Assertion	eqle	$$⊢\left(A\in ℝ\wedge A=B\right)\to A\le B$$

Proof

Step	Hyp	Ref	Expression
1		leid	$$⊢A\in ℝ\to A\le A$$
2		breq2	$$⊢A=B\to \left(A\le A\leftrightarrow A\le B\right)$$
3	2	biimpac	$$⊢\left(A\le A\wedge A=B\right)\to A\le B$$
4	1 3	sylan	$$⊢\left(A\in ℝ\wedge A=B\right)\to A\le B$$