Theorem entr3i

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

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

Proof

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