Theorem letr

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

	Ref	Expression
Assertion	letr	|- ( ( 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	2	adantr	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ A <_ B ) -> ( B <_ C <-> ( B < C \/ B = C ) ) )
4		leltletr	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <_ B /\ B < C ) -> A <_ C ) )
5	4	expdimp	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ A <_ B ) -> ( B < C -> A <_ C ) )
6		breq2	|- ( B = C -> ( A <_ B <-> A <_ C ) )
7	6	biimpcd	|- ( A <_ B -> ( B = C -> A <_ C ) )
8	7	adantl	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ A <_ B ) -> ( B = C -> A <_ C ) )
9	5 8	jaod	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ A <_ B ) -> ( ( B < C \/ B = C ) -> A <_ C ) )
10	3 9	sylbid	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ A <_ B ) -> ( B <_ C -> A <_ C ) )
11	10	expimpd	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <_ B /\ B <_ C ) -> A <_ C ) )