Metamath Proof Explorer

Theorem leltletr

Description: Transitive law, weaker form of lelttr . (Contributed by AV, 14-Oct-2018)

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

Proof

Step Hyp Ref Expression
1 3simpb ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ∈ ℝ ∧ C ∈ ℝ
2 lelttr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ≤ B ∧ B < C → A < C
3 ltle ⊢ A ∈ ℝ ∧ C ∈ ℝ → A < C → A ≤ C
4 1 2 3 sylsyld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ≤ B ∧ B < C → A ≤ C