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

Metamath Proof Explorer

Theorem lttrii

Description: 'Less than' is transitive. (Contributed by SN, 26-Aug-2025)

Ref Expression
Hypotheses lttrii.a ⊢ 𝐴 ∈ ℝ
lttrii.b ⊢ 𝐵 ∈ ℝ
lttrii.c ⊢ 𝐶 ∈ ℝ
lttrii.1 ⊢ 𝐴 < 𝐵
lttrii.2 ⊢ 𝐵 < 𝐶
Assertion lttrii 𝐴 < 𝐶

Proof

Step Hyp Ref Expression
1 lttrii.a ⊢ 𝐴 ∈ ℝ
2 lttrii.b ⊢ 𝐵 ∈ ℝ
3 lttrii.c ⊢ 𝐶 ∈ ℝ
4 lttrii.1 ⊢ 𝐴 < 𝐵
5 lttrii.2 ⊢ 𝐵 < 𝐶
6 1 2 3 lttri ⊢ ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 )
7 4 5 6 mp2an ⊢ 𝐴 < 𝐶