Metamath Proof Explorer


Theorem sotr2

Description: A transitivity relation. (Read B <_ C and C < D implies B < D .) (Contributed by Mario Carneiro, 10-May-2013)

Ref Expression
Assertion sotr2 R Or A B A C A D A ¬ C R B C R D B R D

Proof

Step Hyp Ref Expression
1 sotric R Or A C A B A C R B ¬ C = B B R C
2 1 ancom2s R Or A B A C A C R B ¬ C = B B R C
3 2 3adantr3 R Or A B A C A D A C R B ¬ C = B B R C
4 3 con2bid R Or A B A C A D A C = B B R C ¬ C R B
5 breq1 C = B C R D B R D
6 5 biimpd C = B C R D B R D
7 6 a1i R Or A B A C A D A C = B C R D B R D
8 sotr R Or A B A C A D A B R C C R D B R D
9 8 expd R Or A B A C A D A B R C C R D B R D
10 7 9 jaod R Or A B A C A D A C = B B R C C R D B R D
11 4 10 sylbird R Or A B A C A D A ¬ C R B C R D B R D
12 11 impd R Or A B A C A D A ¬ C R B C R D B R D