Metamath Proof Explorer

Theorem ltleletr

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

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

Proof

Step Hyp Ref Expression
1 3simpb ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A∈ℝ∧C∈ℝ
2 ltletr ⊢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