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 leltletr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ≤ B ∧ B < C → A ≤ C
5 4 expdimp ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A ≤ B → B < C → A ≤ C
6 breq2 ⊢ B = C → A ≤ B ↔ A ≤ C
7 6 biimpcd ⊢ A ≤ B → B = C → A ≤ C
8 7 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A ≤ B → B = C → A ≤ C
9 5 8 jaod ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A ≤ B → B < C ∨ B = C → A ≤ C
10 3 9 sylbid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A ≤ B → B ≤ C → A ≤ C
11 10 expimpd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ≤ B ∧ B ≤ C → A ≤ C