Metamath Proof Explorer

Theorem potr

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

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

Step	Hyp	Ref	Expression
1		pocl	\|- ( R Po A -> ( ( B e. A /\ C e. A /\ D e. A ) -> ( -. B R B /\ ( ( B R C /\ C R D ) -> B R D ) ) ) )
2	1	imp	\|- ( ( R Po A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( -. B R B /\ ( ( B R C /\ C R D ) -> B R D ) ) )
3	2	simprd	\|- ( ( R Po A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( ( B R C /\ C R D ) -> B R D ) )

Step

Hyp

Ref

Expression

 |-  ( R Po A -> ( ( B e. A /\ C e. A /\ D e. A ) -> ( -. B R B /\ ( ( B R C /\ C R D ) -> B R D ) ) ) )

 |-  ( ( R Po A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( -. B R B /\ ( ( B R C /\ C R D ) -> B R D ) ) )

 |-  ( ( R Po A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( ( B R C /\ C R D ) -> B R D ) )