Metamath Proof Explorer

Theorem leltletr

Description: Transitive law, weaker form of lelttr . (Contributed by AV, 14-Oct-2018)

Ref Expression
Assertion leltletr 
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <_ B /\ B < C ) -> A <_ C ) )

Proof

Step Hyp Ref Expression
1 3simpb 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A e. RR /\ C e. RR ) )
2 lelttr 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <_ B /\ B < C ) -> A < C ) )
3 ltle 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A < C -> A <_ C ) )
4 1 2 3 sylsyld 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <_ B /\ B < C ) -> A <_ C ) )