Metamath Proof Explorer

Theorem eqvreltrrel

Description: An equivalence relation is transitive. (Contributed by Peter Mazsa, 29-Dec-2021)

Ref Expression
Assertion eqvreltrrel 
|- ( EqvRel R -> TrRel R )

Proof

Step Hyp Ref Expression
1 df-eqvrel 
 |-  ( EqvRel R <-> ( RefRel R /\ SymRel R /\ TrRel R ) )
2 1 simp3bi 
 |-  ( EqvRel R -> TrRel R )