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