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	⊢ 𝐴 < 𝐶