Theorem ertr3d

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

	Ref	Expression
Hypotheses	ersymb.1	$$⊢\phi \to R\mathrm{Er}X$$
	ertr3d.5	$$⊢\phi \to BRA$$
	ertr3d.6	$$⊢\phi \to BRC$$
Assertion	ertr3d	$$⊢\phi \to ARC$$

Proof

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