Metamath Proof Explorer

Theorem po2nr

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

Ref Expression
Assertion po2nr 
|- ( ( R Po A /\ ( B e. A /\ C e. A ) ) -> -. ( B R C /\ C R B ) )

Proof

Step Hyp Ref Expression
1 poirr 
 |-  ( ( R Po A /\ B e. A ) -> -. B R B )
2 1 adantrr 
 |-  ( ( R Po A /\ ( B e. A /\ C e. A ) ) -> -. B R B )
3 potr 
 |-  ( ( R Po A /\ ( B e. A /\ C e. A /\ B e. A ) ) -> ( ( B R C /\ C R B ) -> B R B ) )
4 3 3exp2 
 |-  ( R Po A -> ( B e. A -> ( C e. A -> ( B e. A -> ( ( B R C /\ C R B ) -> B R B ) ) ) ) )
5 4 com34 
 |-  ( R Po A -> ( B e. A -> ( B e. A -> ( C e. A -> ( ( B R C /\ C R B ) -> B R B ) ) ) ) )
6 5 pm2.43d 
 |-  ( R Po A -> ( B e. A -> ( C e. A -> ( ( B R C /\ C R B ) -> B R B ) ) ) )
7 6 imp32 
 |-  ( ( R Po A /\ ( B e. A /\ C e. A ) ) -> ( ( B R C /\ C R B ) -> B R B ) )
8 2 7 mtod 
 |-  ( ( R Po A /\ ( B e. A /\ C e. A ) ) -> -. ( B R C /\ C R B ) )