This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝑋 𝑅 𝑍 )