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 e. PosetRel /\ A R B /\ B R C ) -> A R C )

Proof

Step Hyp Ref Expression
1 pslem 
 |-  ( R e. PosetRel -> ( ( ( A R B /\ B R C ) -> A R C ) /\ ( A e. U. U. R -> A R A ) /\ ( ( A R B /\ B R A ) -> A = B ) ) )
2 1 simp1d 
 |-  ( R e. PosetRel -> ( ( A R B /\ B R C ) -> A R C ) )
3 2 3impib 
 |-  ( ( R e. PosetRel /\ A R B /\ B R C ) -> A R C )