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

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 e. A /\ C e. A /\ D e. A ) ) -> ( ( -. C R B /\ C R D ) -> B R D ) )

Proof

Step Hyp Ref Expression
1 sotric 
 |-  ( ( R Or A /\ ( C e. A /\ B e. A ) ) -> ( C R B <-> -. ( C = B \/ B R C ) ) )
2 1 ancom2s 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( C R B <-> -. ( C = B \/ B R C ) ) )
3 2 3adantr3 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( C R B <-> -. ( C = B \/ B R C ) ) )
4 3 con2bid 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A /\ D e. 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 e. A /\ C e. A /\ D e. A ) ) -> ( C = B -> ( C R D -> B R D ) ) )
8 sotr 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( ( B R C /\ C R D ) -> B R D ) )
9 8 expd 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( B R C -> ( C R D -> B R D ) ) )
10 7 9 jaod 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( ( C = B \/ B R C ) -> ( C R D -> B R D ) ) )
11 4 10 sylbird 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( -. C R B -> ( C R D -> B R D ) ) )
12 11 impd 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( ( -. C R B /\ C R D ) -> B R D ) )