Metamath Proof Explorer

Theorem letr

Description: Transitive law. (Contributed by NM, 12-Nov-1999)

Ref Expression
Assertion letr ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A≤B∧B≤C→A≤C

Proof

Step Hyp Ref Expression
1 leloe ⊢B∈ℝ∧C∈ℝ→B≤C↔B<C∨B=C
2 1 3adant1 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→B≤C↔B<C∨B=C
3 2 adantr ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧A≤B→B≤C↔B<C∨B=C
4 lelttr ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A≤B∧B<C→A<C
5 ltle ⊢A∈ℝ∧C∈ℝ→A<C→A≤C
6 5 3adant2 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A<C→A≤C
7 4 6 syld ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A≤B∧B<C→A≤C
8 7 expdimp ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧A≤B→B<C→A≤C
9 breq2 ⊢B=C→A≤B↔A≤C
10 9 biimpcd ⊢A≤B→B=C→A≤C
11 10 adantl ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧A≤B→B=C→A≤C
12 8 11 jaod ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧A≤B→B<C∨B=C→A≤C
13 3 12 sylbid ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧A≤B→B≤C→A≤C
14 13 expimpd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A≤B∧B≤C→A≤C