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

Metamath Proof Explorer

Theorem sotr

Description: A strict order relation is a transitive relation. (Contributed by NM, 21-Jan-1996)

		Ref	Expression
	Assertion	sotr	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ) → 𝐵 𝑅 𝐷 ) )

Step	Hyp	Ref	Expression
1		sopo	⊢ ( 𝑅 Or 𝐴 → 𝑅 Po 𝐴 )
2		potr	⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ) → 𝐵 𝑅 𝐷 ) )
3	1 2	sylan	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ) → 𝐵 𝑅 𝐷 ) )