Metamath Proof Explorer

Theorem so3nr

Description: A strict order relation has no 3-cycle loops. (Contributed by NM, 21-Jan-1996)

Ref Expression
Assertion so3nr ⊢ R Or A ∧ B ∈ A ∧ C ∈ A ∧ D ∈ A → ¬ B R C ∧ C R D ∧ D R B

Proof

Step Hyp Ref Expression
1 sopo ⊢ R Or A → R Po A
2 po3nr ⊢ R Po A ∧ B ∈ A ∧ C ∈ A ∧ D ∈ A → ¬ B R C ∧ C R D ∧ D R B
3 1 2 sylan ⊢ R Or A ∧ B ∈ A ∧ C ∈ A ∧ D ∈ A → ¬ B R C ∧ C R D ∧ D R B