Theorem eqvreltrrel

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

	Ref	Expression
Assertion	eqvreltrrel	⊢ ( EqvRel 𝑅 → TrRel 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		df-eqvrel	⊢ ( EqvRel 𝑅 ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅 ) )
2	1	simp3bi	⊢ ( EqvRel 𝑅 → TrRel 𝑅 )