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 A C A ¬ B R C C R B

Proof

Step Hyp Ref Expression
1 poirr R Po A B A ¬ B R B
2 1 adantrr R Po A B A C A ¬ B R B
3 potr R Po A B A C A B A B R C C R B B R B
4 3 3exp2 R Po A B A C A B A B R C C R B B R B
5 4 com34 R Po A B A B A C A B R C C R B B R B
6 5 pm2.43d R Po A B A C A B R C C R B B R B
7 6 imp32 R Po A B A C A B R C C R B B R B
8 2 7 mtod R Po A B A C A ¬ B R C C R B