Metamath Proof Explorer


Theorem letr

Description: Transitive law. (Contributed by NM, 12-Nov-1999)

Ref Expression
Assertion letr 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 2 adantr A B C A B B C B < C B = C
4 lelttr A B C A B B < C A < C
5 ltle A C A < C A C
6 5 3adant2 A B C A < C A C
7 4 6 syld A B C A B B < C A C
8 7 expdimp A B C A B B < C A C
9 breq2 B = C A B A C
10 9 biimpcd A B B = C A C
11 10 adantl A B C A B B = C A C
12 8 11 jaod A B C A B B < C B = C A C
13 3 12 sylbid A B C A B B C A C
14 13 expimpd A B C A B B C A C