Theorem sotrd

Description: Transitivity law for strict orderings, deduction form. (Contributed by Scott Fenton, 24-Nov-2021)

	Ref	Expression
Hypotheses	sotrd.1	|- ( ph -> R Or A )
	sotrd.2	|- ( ph -> X e. A )
	sotrd.3	|- ( ph -> Y e. A )
	sotrd.4	|- ( ph -> Z e. A )
	sotrd.5	|- ( ph -> X R Y )
	sotrd.6	|- ( ph -> Y R Z )
Assertion	sotrd	|- ( ph -> X R Z )

Proof

Step	Hyp	Ref	Expression
1		sotrd.1	|- ( ph -> R Or A )
2		sotrd.2	|- ( ph -> X e. A )
3		sotrd.3	|- ( ph -> Y e. A )
4		sotrd.4	|- ( ph -> Z e. A )
5		sotrd.5	|- ( ph -> X R Y )
6		sotrd.6	|- ( ph -> Y R Z )
7		sotr	|- ( ( R Or A /\ ( X e. A /\ Y e. A /\ Z e. A ) ) -> ( ( X R Y /\ Y R Z ) -> X R Z ) )
8	1 2 3 4 7	syl13anc	|- ( ph -> ( ( X R Y /\ Y R Z ) -> X R Z ) )
9	5 6 8	mp2and	|- ( ph -> X R Z )