Theorem ertr4d

Description: A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014)

	Ref	Expression
Hypotheses	ersymb.1	$$⊢\phi \to R\mathrm{Er}X$$
	ertr4d.5	$$⊢\phi \to ARB$$
	ertr4d.6	$$⊢\phi \to CRB$$
Assertion	ertr4d	$$⊢\phi \to ARC$$

Proof

Step	Hyp	Ref	Expression
1		ersymb.1	$$⊢\phi \to R\mathrm{Er}X$$
2		ertr4d.5	$$⊢\phi \to ARB$$
3		ertr4d.6	$$⊢\phi \to CRB$$
4	1 3	ersym	$$⊢\phi \to BRC$$
5	1 2 4	ertrd	$$⊢\phi \to ARC$$