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 𝐴 ∧ ( 𝐵𝐴𝐶𝐴𝐷𝐴 ) ) → ( ( 𝐵 𝑅 𝐶𝐶 𝑅 𝐷 ) → 𝐵 𝑅 𝐷 ) )

Proof

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