This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )