Theorem entr2i

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

	Ref	Expression
Hypotheses	entr2i.1	⊢ 𝐴 ≈ 𝐵
	entr2i.2	⊢ 𝐵 ≈ 𝐶
Assertion	entr2i	⊢ 𝐶 ≈ 𝐴

Proof

Step	Hyp	Ref	Expression
1		entr2i.1	⊢ 𝐴 ≈ 𝐵
2		entr2i.2	⊢ 𝐵 ≈ 𝐶
3	1 2	entri	⊢ 𝐴 ≈ 𝐶
4	3	ensymi	⊢ 𝐶 ≈ 𝐴