Metamath Proof Explorer


Theorem potr

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

Ref Expression
Assertion potr RPoABACADABRCCRDBRD

Proof

Step Hyp Ref Expression
1 pocl RPoABACADA¬BRBBRCCRDBRD
2 1 imp RPoABACADA¬BRBBRCCRDBRD
3 2 simprd RPoABACADABRCCRDBRD