Theorem sotri

Description: A strict order relation is a transitive relation. (Contributed by NM, 10-Feb-1996) (Revised by Mario Carneiro, 10-May-2013)

	Ref	Expression
Hypotheses	soi.1	|- R Or S
	soi.2	|- R C_ ( S X. S )
Assertion	sotri	|- ( ( A R B /\ B R C ) -> A R C )

Proof

Step	Hyp	Ref	Expression
1		soi.1	|- R Or S
2		soi.2	|- R C_ ( S X. S )
3	2	brel	|- ( A R B -> ( A e. S /\ B e. S ) )
4	3	simpld	|- ( A R B -> A e. S )
5	2	brel	|- ( B R C -> ( B e. S /\ C e. S ) )
6	4 5	anim12i	|- ( ( A R B /\ B R C ) -> ( A e. S /\ ( B e. S /\ C e. S ) ) )
7		sotr	|- ( ( R Or S /\ ( A e. S /\ B e. S /\ C e. S ) ) -> ( ( A R B /\ B R C ) -> A R C ) )
8	1 7	mpan	|- ( ( A e. S /\ B e. S /\ C e. S ) -> ( ( A R B /\ B R C ) -> A R C ) )
9	8	3expb	|- ( ( A e. S /\ ( B e. S /\ C e. S ) ) -> ( ( A R B /\ B R C ) -> A R C ) )
10	6 9	mpcom	|- ( ( A R B /\ B R C ) -> A R C )