Metamath Proof Explorer

Theorem eqvreltrrel

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

		Ref	Expression
	Assertion	eqvreltrrel	$⊢ EqvRel R \to TrRel R$

Step	Hyp	Ref	Expression
1		df-eqvrel	$⊢ EqvRel R \leftrightarrow (RefRel R \land SymRel R \land TrRel R)$
2	1	simp3bi	$⊢ EqvRel R \to TrRel R$