Theorem enen2

Description: Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003)

	Ref	Expression
Assertion	enen2	$$⊢A\approx B\to \left(C\approx A\leftrightarrow C\approx B\right)$$

Proof

Step	Hyp	Ref	Expression
1		entr	$$⊢\left(C\approx A\wedge A\approx B\right)\to C\approx B$$
2	1	ancoms	$$⊢\left(A\approx B\wedge C\approx A\right)\to C\approx B$$
3		ensym	$$⊢A\approx B\to B\approx A$$
4		entr	$$⊢\left(C\approx B\wedge B\approx A\right)\to C\approx A$$
5	4	ancoms	$$⊢\left(B\approx A\wedge C\approx B\right)\to C\approx A$$
6	3 5	sylan	$$⊢\left(A\approx B\wedge C\approx B\right)\to C\approx A$$
7	2 6	impbida	$$⊢A\approx B\to \left(C\approx A\leftrightarrow C\approx B\right)$$