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