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

Metamath Proof Explorer

Theorem ltletr

Description: Transitive law. (Contributed by NM, 25-Aug-1999)

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

Proof

Step Hyp Ref Expression
1 leloe 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B <_ C <-> ( B < C \/ B = C ) ) )
2 1 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B <_ C <-> ( B < C \/ B = C ) ) )
3 lttr 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) -> A < C ) )
4 3 expcomd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B < C -> ( A < B -> A < C ) ) )
5 breq2 
 |-  ( B = C -> ( A < B <-> A < C ) )
6 5 biimpd 
 |-  ( B = C -> ( A < B -> A < C ) )
7 6 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B = C -> ( A < B -> A < C ) ) )
8 4 7 jaod 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( B < C \/ B = C ) -> ( A < B -> A < C ) ) )
9 2 8 sylbid 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B <_ C -> ( A < B -> A < C ) ) )
10 9 impcomd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B <_ C ) -> A < C ) )