Theorem sotrd

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

	Ref	Expression
Hypotheses	sotrd.1	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
	sotrd.2	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	sotrd.3	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
	sotrd.4	⊢ ( 𝜑 → 𝑍 ∈ 𝐴 )
	sotrd.5	⊢ ( 𝜑 → 𝑋 𝑅 𝑌 )
	sotrd.6	⊢ ( 𝜑 → 𝑌 𝑅 𝑍 )
Assertion	sotrd	⊢ ( 𝜑 → 𝑋 𝑅 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		sotrd.1	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
2		sotrd.2	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
3		sotrd.3	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
4		sotrd.4	⊢ ( 𝜑 → 𝑍 ∈ 𝐴 )
5		sotrd.5	⊢ ( 𝜑 → 𝑋 𝑅 𝑌 )
6		sotrd.6	⊢ ( 𝜑 → 𝑌 𝑅 𝑍 )
7		sotr	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ) ) → ( ( 𝑋 𝑅 𝑌 ∧ 𝑌 𝑅 𝑍 ) → 𝑋 𝑅 𝑍 ) )
8	1 2 3 4 7	syl13anc	⊢ ( 𝜑 → ( ( 𝑋 𝑅 𝑌 ∧ 𝑌 𝑅 𝑍 ) → 𝑋 𝑅 𝑍 ) )
9	5 6 8	mp2and	⊢ ( 𝜑 → 𝑋 𝑅 𝑍 )