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 e. A /\ C e. A /\ D e. 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 e. A /\ C e. A /\ D e. A ) ) -> -. ( B R C /\ C R D /\ D R B ) )
3 1 2 sylan 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> -. ( B R C /\ C R D /\ D R B ) )