Metamath Proof Explorer


Theorem ltletr

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

Ref Expression
Assertion ltletr A B C A < B B C A < C

Proof

Step Hyp Ref Expression
1 leloe B C B C B < C B = C
2 1 3adant1 A B C B C B < C B = C
3 lttr A B C A < B B < C A < C
4 3 expcomd A B C 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 B C B = C A < B A < C
8 4 7 jaod A B C B < C B = C A < B A < C
9 2 8 sylbid A B C B C A < B A < C
10 9 impcomd A B C A < B B C A < C