Theorem sotr

Description: A strict order relation is a transitive relation. (Contributed by NM, 21-Jan-1996)

	Ref	Expression
Assertion	sotr	$$⊢\left(R\mathrm{Or}A\wedge \left(B\in A\wedge C\in A\wedge D\in A\right)\right)\to \left(\left(BRC\wedge CRD\right)\to BRD\right)$$

Proof

Step	Hyp	Ref	Expression
1		sopo	$$⊢R\mathrm{Or}A\to R\mathrm{Po}A$$
2		potr	$$⊢\left(R\mathrm{Po}A\wedge \left(B\in A\wedge C\in A\wedge D\in A\right)\right)\to \left(\left(BRC\wedge CRD\right)\to BRD\right)$$
3	1 2	sylan	$$⊢\left(R\mathrm{Or}A\wedge \left(B\in A\wedge C\in A\wedge D\in A\right)\right)\to \left(\left(BRC\wedge CRD\right)\to BRD\right)$$