Theorem lttrii

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

	Ref	Expression
Hypotheses	lttrii.a	$$⊢A\in ℝ$$
	lttrii.b	$$⊢B\in ℝ$$
	lttrii.c	$$⊢C\in ℝ$$
	lttrii.1	$$⊢A<B$$
	lttrii.2	$$⊢B<C$$
Assertion	lttrii	$$⊢A<C$$

Proof

Step	Hyp	Ref	Expression
1		lttrii.a	$$⊢A\in ℝ$$
2		lttrii.b	$$⊢B\in ℝ$$
3		lttrii.c	$$⊢C\in ℝ$$
4		lttrii.1	$$⊢A<B$$
5		lttrii.2	$$⊢B<C$$
6	1 2 3	lttri	$$⊢\left(A<B\wedge B<C\right)\to A<C$$
7	4 5 6	mp2an	$$⊢A<C$$