Metamath Proof Explorer

Theorem lelttr

Description: Transitive law. (Contributed by NM, 23-May-1999)

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

Proof

Step Hyp Ref Expression
1 leloe ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ↔ A < B ∨ A = B
2 1 3adant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ≤ B ↔ A < B ∨ A = B
3 lttr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < B ∧ B < C → A < C
4 3 expd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < B → B < C → A < C
5 breq1 ⊢ A = B → A < C ↔ B < C
6 5 biimprd ⊢ A = B → B < C → A < C
7 6 a1i ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A = B → B < C → A < C
8 4 7 jaod ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < B ∨ A = B → B < C → A < C
9 2 8 sylbid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ≤ B → B < C → A < C
10 9 impd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ≤ B ∧ B < C → A < C