Metamath Proof Explorer


Theorem leltletr

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

Ref Expression
Assertion leltletr ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴𝐵𝐵 < 𝐶 ) → 𝐴𝐶 ) )

Proof

Step Hyp Ref Expression
1 3simpb ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) )
2 lelttr ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴𝐵𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
3 ltle ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 < 𝐶𝐴𝐶 ) )
4 1 2 3 sylsyld ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴𝐵𝐵 < 𝐶 ) → 𝐴𝐶 ) )