Metamath Proof Explorer


Theorem po3nr

Description: A partial order has no 3-cycle loops. (Contributed by NM, 27-Mar-1997)

Ref Expression
Assertion po3nr
|- ( ( R Po 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 po2nr
 |-  ( ( R Po A /\ ( B e. A /\ D e. A ) ) -> -. ( B R D /\ D R B ) )
2 1 3adantr2
 |-  ( ( R Po A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> -. ( B R D /\ D R B ) )
3 df-3an
 |-  ( ( B R C /\ C R D /\ D R B ) <-> ( ( B R C /\ C R D ) /\ D R B ) )
4 potr
 |-  ( ( R Po A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( ( B R C /\ C R D ) -> B R D ) )
5 4 anim1d
 |-  ( ( R Po A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( ( ( B R C /\ C R D ) /\ D R B ) -> ( B R D /\ D R B ) ) )
6 3 5 syl5bi
 |-  ( ( R Po A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( ( B R C /\ C R D /\ D R B ) -> ( B R D /\ D R B ) ) )
7 2 6 mtod
 |-  ( ( R Po A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> -. ( B R C /\ C R D /\ D R B ) )