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 ⊢ A ∈ ℝ
lttrii.b ⊢ B ∈ ℝ
lttrii.c ⊢ C ∈ ℝ
lttrii.1 ⊢ A < B
lttrii.2 ⊢ B < C
Assertion lttrii ⊢ A < C

Proof

Step Hyp Ref Expression
1 lttrii.a ⊢ A ∈ ℝ
2 lttrii.b ⊢ B ∈ ℝ
3 lttrii.c ⊢ C ∈ ℝ
4 lttrii.1 ⊢ A < B
5 lttrii.2 ⊢ B < C
6 1 2 3 lttri ⊢ A < B ∧ B < C → A < C
7 4 5 6 mp2an ⊢ A < C