Theorem eqlei2

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

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

Proof

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