Metamath Proof Explorer

Theorem pstr

Description: A poset is transitive. (Contributed by NM, 12-May-2008) (Revised by Mario Carneiro, 30-Apr-2015)

		Ref	Expression
	Assertion	pstr	$⊢ (R \in PosetRel \land A R B \land B R C) \to A R C$

Step	Hyp	Ref	Expression
1		pslem	$⊢ R \in PosetRel \to (((A R B \land B R C) \to A R C) \land (A \in ⋃ ⋃ R \to A R A) \land ((A R B \land B R A) \to A = B))$
2	1	simp1d	$⊢ R \in PosetRel \to ((A R B \land B R C) \to A R C)$
3	2	3impib	$⊢ (R \in PosetRel \land A R B \land B R C) \to A R C$