Theorem sotrd

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

	Ref	Expression
Hypotheses	sotrd.1	$$⊢\phi \to R\mathrm{Or}A$$
	sotrd.2	$$⊢\phi \to X\in A$$
	sotrd.3	$$⊢\phi \to Y\in A$$
	sotrd.4	$$⊢\phi \to Z\in A$$
	sotrd.5	$$⊢\phi \to XRY$$
	sotrd.6	$$⊢\phi \to YRZ$$
Assertion	sotrd	$$⊢\phi \to XRZ$$

Proof

Step	Hyp	Ref	Expression
1		sotrd.1	$$⊢\phi \to R\mathrm{Or}A$$
2		sotrd.2	$$⊢\phi \to X\in A$$
3		sotrd.3	$$⊢\phi \to Y\in A$$
4		sotrd.4	$$⊢\phi \to Z\in A$$
5		sotrd.5	$$⊢\phi \to XRY$$
6		sotrd.6	$$⊢\phi \to YRZ$$
7		sotr	$$⊢\left(R\mathrm{Or}A\wedge \left(X\in A\wedge Y\in A\wedge Z\in A\right)\right)\to \left(\left(XRY\wedge YRZ\right)\to XRZ\right)$$
8	1 2 3 4 7	syl13anc	$$⊢\phi \to \left(\left(XRY\wedge YRZ\right)\to XRZ\right)$$
9	5 6 8	mp2and	$$⊢\phi \to XRZ$$