Theorem entr2i

Description: A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004)

	Ref	Expression
Hypotheses	entr2i.1	$$⊢A\approx B$$
	entr2i.2	$$⊢B\approx C$$
Assertion	entr2i	$$⊢C\approx A$$

Proof

Step	Hyp	Ref	Expression
1		entr2i.1	$$⊢A\approx B$$
2		entr2i.2	$$⊢B\approx C$$
3	1 2	entri	$$⊢A\approx C$$
4	3	ensymi	$$⊢C\approx A$$