Theorem eqlei

Description: Equality implies 'less than or equal to'. (Contributed by NM, 23-May-1999) (Revised by Alexander van der Vekens, 20-Mar-2018)

	Ref	Expression
Hypothesis	lt.1	⊢ 𝐴 ∈ ℝ
Assertion	eqlei	⊢ ( 𝐴 = 𝐵 → 𝐴 ≤ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		lt.1	⊢ 𝐴 ∈ ℝ
2		eleq1a	⊢ ( 𝐴 ∈ ℝ → ( 𝐵 = 𝐴 → 𝐵 ∈ ℝ ) )
3	1 2	ax-mp	⊢ ( 𝐵 = 𝐴 → 𝐵 ∈ ℝ )
4	3	eqcoms	⊢ ( 𝐴 = 𝐵 → 𝐵 ∈ ℝ )
5		letri3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 = 𝐵 ↔ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴 ) ) )
6	1 5	mpan	⊢ ( 𝐵 ∈ ℝ → ( 𝐴 = 𝐵 ↔ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴 ) ) )
7		simpl	⊢ ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴 ) → 𝐴 ≤ 𝐵 )
8	6 7	biimtrdi	⊢ ( 𝐵 ∈ ℝ → ( 𝐴 = 𝐵 → 𝐴 ≤ 𝐵 ) )
9	4 8	mpcom	⊢ ( 𝐴 = 𝐵 → 𝐴 ≤ 𝐵 )