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 biimtrid 
 |-  ( ( 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 ) )