Theorem eqvreltrrel

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

	Ref	Expression
Assertion	eqvreltrrel	$$⊢EqvRelR\to TrRelR$$

Proof

Step	Hyp	Ref	Expression
1		df-eqvrel	$$⊢EqvRelR\leftrightarrow \left(RefRelR\wedge SymRelR\wedge TrRelR\right)$$
2	1	simp3bi	$$⊢EqvRelR\to TrRelR$$