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 \land (B \in A \land C \in A \land D \in A)) \to ((\neg C R B \land C R D) \to B R D)$

Step	Hyp	Ref	Expression
1		sotric	$⊢ (R Or A \land (C \in A \land B \in A)) \to (C R B \leftrightarrow \neg (C = B \lor B R C))$
2	1	ancom2s	$⊢ (R Or A \land (B \in A \land C \in A)) \to (C R B \leftrightarrow \neg (C = B \lor B R C))$
3	2	3adantr3	$⊢ (R Or A \land (B \in A \land C \in A \land D \in A)) \to (C R B \leftrightarrow \neg (C = B \lor B R C))$
4	3	con2bid	$⊢ (R Or A \land (B \in A \land C \in A \land D \in A)) \to ((C = B \lor B R C) \leftrightarrow \neg C R B)$
5		breq1	$⊢ C = B \to (C R D \leftrightarrow B R D)$
6	5	biimpd	$⊢ C = B \to (C R D \to B R D)$
7	6	a1i	$⊢ (R Or A \land (B \in A \land C \in A \land D \in A)) \to (C = B \to (C R D \to B R D))$
8		sotr	$⊢ (R Or A \land (B \in A \land C \in A \land D \in A)) \to ((B R C \land C R D) \to B R D)$
9	8	expd	$⊢ (R Or A \land (B \in A \land C \in A \land D \in A)) \to (B R C \to (C R D \to B R D))$
10	7 9	jaod	$⊢ (R Or A \land (B \in A \land C \in A \land D \in A)) \to ((C = B \lor B R C) \to (C R D \to B R D))$
11	4 10	sylbird	$⊢ (R Or A \land (B \in A \land C \in A \land D \in A)) \to (\neg C R B \to (C R D \to B R D))$
12	11	impd	$⊢ (R Or A \land (B \in A \land C \in A \land D \in A)) \to ((\neg C R B \land C R D) \to B R D)$

Metamath Proof Explorer