This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lenlteq

Description: 'less than or equal to' but not 'less than' implies 'equal' . (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses lenlteq.1 ⊢ φ → A ∈ ℝ
lenlteq.2 ⊢ φ → B ∈ ℝ
lenlteq.3 ⊢ φ → A ≤ B
lenlteq.4 ⊢ φ → ¬ A < B
Assertion lenlteq ⊢ φ → A = B

Proof

Step Hyp Ref Expression
1 lenlteq.1 ⊢ φ → A ∈ ℝ
2 lenlteq.2 ⊢ φ → B ∈ ℝ
3 lenlteq.3 ⊢ φ → A ≤ B
4 lenlteq.4 ⊢ φ → ¬ A < B
5 3 4 jca ⊢ φ → A ≤ B ∧ ¬ A < B
6 eqlelt ⊢ A ∈ ℝ ∧ B ∈ ℝ → A = B ↔ A ≤ B ∧ ¬ A < B
7 1 2 6 syl2anc ⊢ φ → A = B ↔ A ≤ B ∧ ¬ A < B
8 5 7 mpbird ⊢ φ → A = B