Metamath Proof Explorer


Theorem ispod

Description: Sufficient conditions for a partial order. (Contributed by NM, 9-Jul-2014)

Ref Expression
Hypotheses ispod.1 φxA¬xRx
ispod.2 φxAyAzAxRyyRzxRz
Assertion ispod φRPoA

Proof

Step Hyp Ref Expression
1 ispod.1 φxA¬xRx
2 ispod.2 φxAyAzAxRyyRzxRz
3 1 3ad2antr1 φxAyAzA¬xRx
4 3 2 jca φxAyAzA¬xRxxRyyRzxRz
5 4 ralrimivvva φxAyAzA¬xRxxRyyRzxRz
6 df-po RPoAxAyAzA¬xRxxRyyRzxRz
7 5 6 sylibr φRPoA