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	|- ( ph -> ( A e. RR /\ B e. RR /\ C e. RR ) )
	lelttrdi.l	|- ( ph -> B <_ C )
Assertion	lelttrdi	|- ( ph -> ( A < B -> A < C ) )

Proof

Step	Hyp	Ref	Expression
1		lelttrdi.r	|- ( ph -> ( A e. RR /\ B e. RR /\ C e. RR ) )
2		lelttrdi.l	|- ( ph -> B <_ C )
3	1	simp1d	|- ( ph -> A e. RR )
4	3	adantr	|- ( ( ph /\ A < B ) -> A e. RR )
5	1	simp2d	|- ( ph -> B e. RR )
6	5	adantr	|- ( ( ph /\ A < B ) -> B e. RR )
7	1	simp3d	|- ( ph -> C e. RR )
8	7	adantr	|- ( ( ph /\ A < B ) -> C e. RR )
9		simpr	|- ( ( ph /\ A < B ) -> A < B )
10	2	adantr	|- ( ( ph /\ A < B ) -> B <_ C )
11	4 6 8 9 10	ltletrd	|- ( ( ph /\ A < B ) -> A < C )
12	11	ex	|- ( ph -> ( A < B -> A < C ) )