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	$⊢ φ \to (A \in ℝ \land B \in ℝ \land C \in ℝ)$
	lelttrdi.l	$⊢ φ \to B \leq C$
Assertion	lelttrdi	$⊢ φ \to (A < B \to A < C)$

Proof

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

Metamath Proof Explorer

Theorem lelttrdi

Proof