Theorem lelttrdi

Description: If a number is less than another number, and the other number is less than or equal to a third number, the first number is less than the third number. (Contributed by Alexander van der Vekens, 24-Mar-2018)

	Ref	Expression
Hypotheses	lelttrdi.r	$$⊢\phi \to \left(A\in ℝ\wedge B\in ℝ\wedge C\in ℝ\right)$$
	lelttrdi.l	$$⊢\phi \to B\le C$$
Assertion	lelttrdi	$$⊢\phi \to \left(A<B\to A<C\right)$$

Proof

Step	Hyp	Ref	Expression
1		lelttrdi.r	$$⊢\phi \to \left(A\in ℝ\wedge B\in ℝ\wedge C\in ℝ\right)$$
2		lelttrdi.l	$$⊢\phi \to B\le C$$
3	1	simp1d	$$⊢\phi \to A\in ℝ$$
4	3	adantr	$$⊢\left(\phi \wedge A<B\right)\to A\in ℝ$$
5	1	simp2d	$$⊢\phi \to B\in ℝ$$
6	5	adantr	$$⊢\left(\phi \wedge A<B\right)\to B\in ℝ$$
7	1	simp3d	$$⊢\phi \to C\in ℝ$$
8	7	adantr	$$⊢\left(\phi \wedge A<B\right)\to C\in ℝ$$
9		simpr	$$⊢\left(\phi \wedge A<B\right)\to A<B$$
10	2	adantr	$$⊢\left(\phi \wedge A<B\right)\to B\le C$$
11	4 6 8 9 10	ltletrd	$$⊢\left(\phi \wedge A<B\right)\to A<C$$
12	11	ex	$$⊢\phi \to \left(A<B\to A<C\right)$$