This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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