Theorem ertr2d

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

	Ref	Expression
Hypotheses	ersymb.1	$$⊢\phi \to R\mathrm{Er}X$$
	ertrd.5	$$⊢\phi \to ARB$$
	ertrd.6	$$⊢\phi \to BRC$$
Assertion	ertr2d	$$⊢\phi \to CRA$$

Proof

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