Theorem ertrd

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	ertrd	$$⊢\phi \to ARC$$

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	ertr	$$⊢\phi \to \left(\left(ARB\wedge BRC\right)\to ARC\right)$$
5	2 3 4	mp2and	$$⊢\phi \to ARC$$