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