Metamath Proof Explorer


Theorem poirr

Description: A partial order is irreflexive. (Contributed by NM, 27-Mar-1997)

Ref Expression
Assertion poirr R Po A B A ¬ B R B

Proof

Step Hyp Ref Expression
1 df-3an B A B A B A B A B A B A
2 anabs1 B A B A B A B A B A
3 anidm B A B A B A
4 1 2 3 3bitrri B A B A B A B A
5 pocl R Po A B A B A B A ¬ B R B B R B B R B B R B
6 5 imp R Po A B A B A B A ¬ B R B B R B B R B B R B
7 6 simpld R Po A B A B A B A ¬ B R B
8 4 7 sylan2b R Po A B A ¬ B R B