Theorem eqvreltr4d

Description: A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014) (Revised by Peter Mazsa, 2-Jun-2019)

	Ref	Expression
Hypotheses	eqvreltr4d.1	$$⊢\phi \to EqvRelR$$
	eqvreltr4d.2	$$⊢\phi \to ARB$$
	eqvreltr4d.3	$$⊢\phi \to CRB$$
Assertion	eqvreltr4d	$$⊢\phi \to ARC$$

Proof

Step	Hyp	Ref	Expression
1		eqvreltr4d.1	$$⊢\phi \to EqvRelR$$
2		eqvreltr4d.2	$$⊢\phi \to ARB$$
3		eqvreltr4d.3	$$⊢\phi \to CRB$$
4	1 3	eqvrelsym	$$⊢\phi \to BRC$$
5	1 2 4	eqvreltrd	$$⊢\phi \to ARC$$