This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \land (B \in A \land C \in A \land D \in A)) \to ((B R C \land C R D) \to B R D)$

Step	Hyp	Ref	Expression
1		pocl	$⊢ R Po A \to ((B \in A \land C \in A \land D \in A) \to (\neg B R B \land ((B R C \land C R D) \to B R D)))$
2	1	imp	$⊢ (R Po A \land (B \in A \land C \in A \land D \in A)) \to (\neg B R B \land ((B R C \land C R D) \to B R D))$
3	2	simprd	$⊢ (R Po A \land (B \in A \land C \in A \land D \in A)) \to ((B R C \land C R D) \to B R D)$