Metamath Proof Explorer

Theorem ltleletr

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

Ref Expression
Assertion ltleletr 
|- ( ( 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 ltletr 
 |-  ( ( 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 ) )