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

Metamath Proof Explorer

Theorem le2tri3i

Description: Extended trichotomy law for 'less than or equal to'. (Contributed by NM, 14-Aug-2000)

Ref Expression
Hypotheses lt.1 ⊢ A ∈ ℝ
lt.2 ⊢ B ∈ ℝ
lt.3 ⊢ C ∈ ℝ
Assertion le2tri3i ⊢ A ≤ B ∧ B ≤ C ∧ C ≤ A ↔ A = B ∧ B = C ∧ C = A

Proof

Step Hyp Ref Expression
1 lt.1 ⊢ A ∈ ℝ
2 lt.2 ⊢ B ∈ ℝ
3 lt.3 ⊢ C ∈ ℝ
4 2 3 1 letri ⊢ B ≤ C ∧ C ≤ A → B ≤ A
5 1 2 letri3i ⊢ A = B ↔ A ≤ B ∧ B ≤ A
6 5 biimpri ⊢ A ≤ B ∧ B ≤ A → A = B
7 4 6 sylan2 ⊢ A ≤ B ∧ B ≤ C ∧ C ≤ A → A = B
8 7 3impb ⊢ A ≤ B ∧ B ≤ C ∧ C ≤ A → A = B
9 3 1 2 letri ⊢ C ≤ A ∧ A ≤ B → C ≤ B
10 2 3 letri3i ⊢ B = C ↔ B ≤ C ∧ C ≤ B
11 10 biimpri ⊢ B ≤ C ∧ C ≤ B → B = C
12 9 11 sylan2 ⊢ B ≤ C ∧ C ≤ A ∧ A ≤ B → B = C
13 12 3impb ⊢ B ≤ C ∧ C ≤ A ∧ A ≤ B → B = C
14 13 3comr ⊢ A ≤ B ∧ B ≤ C ∧ C ≤ A → B = C
15 1 2 3 letri ⊢ A ≤ B ∧ B ≤ C → A ≤ C
16 1 3 letri3i ⊢ A = C ↔ A ≤ C ∧ C ≤ A
17 16 biimpri ⊢ A ≤ C ∧ C ≤ A → A = C
18 17 eqcomd ⊢ A ≤ C ∧ C ≤ A → C = A
19 15 18 stoic3 ⊢ A ≤ B ∧ B ≤ C ∧ C ≤ A → C = A
20 8 14 19 3jca ⊢ A ≤ B ∧ B ≤ C ∧ C ≤ A → A = B ∧ B = C ∧ C = A
21 1 eqlei ⊢ A = B → A ≤ B
22 2 eqlei ⊢ B = C → B ≤ C
23 3 eqlei ⊢ C = A → C ≤ A
24 21 22 23 3anim123i ⊢ A = B ∧ B = C ∧ C = A → A ≤ B ∧ B ≤ C ∧ C ≤ A
25 20 24 impbii ⊢ A ≤ B ∧ B ≤ C ∧ C ≤ A ↔ A = B ∧ B = C ∧ C = A