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

Metamath Proof Explorer

Theorem ltlecasei

Description: Ordering elimination by cases. (Contributed by NM, 1-Jul-2007) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses ltlecasei.1 ⊢ φ ∧ A < B → ψ
ltlecasei.2 ⊢ φ ∧ B ≤ A → ψ
ltlecasei.3 ⊢ φ → A ∈ ℝ
ltlecasei.4 ⊢ φ → B ∈ ℝ
Assertion ltlecasei ⊢ φ → ψ

Proof

Step Hyp Ref Expression
1 ltlecasei.1 ⊢ φ ∧ A < B → ψ
2 ltlecasei.2 ⊢ φ ∧ B ≤ A → ψ
3 ltlecasei.3 ⊢ φ → A ∈ ℝ
4 ltlecasei.4 ⊢ φ → B ∈ ℝ
5 lelttric ⊢ B ∈ ℝ ∧ A ∈ ℝ → B ≤ A ∨ A < B
6 4 3 5 syl2anc ⊢ φ → B ≤ A ∨ A < B
7 2 1 6 mpjaodan ⊢ φ → ψ