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

Metamath Proof Explorer

Theorem lttri4d

Description: Trichotomy law for 'less than'. (Contributed by NM, 20-Sep-2007) (Proof shortened by Andrew Salmon, 19-Nov-2011)

Ref Expression
Hypotheses ltd.1 ⊢ φ → A ∈ ℝ
ltd.2 ⊢ φ → B ∈ ℝ
Assertion lttri4d ⊢ φ → A < B ∨ A = B ∨ B < A

Proof

Step Hyp Ref Expression
1 ltd.1 ⊢ φ → A ∈ ℝ
2 ltd.2 ⊢ φ → B ∈ ℝ
3 lttri4 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ∨ A = B ∨ B < A
4 1 2 3 syl2anc ⊢ φ → A < B ∨ A = B ∨ B < A