Theorem eqeq2d

Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993) Allow shortening of eqeq2 . (Revised by Wolf Lammen, 19-Nov-2019)

	Ref	Expression
Hypothesis	eqeq2d.1	$$⊢\phi \to A=B$$
Assertion	eqeq2d	$$⊢\phi \to \left(C=A\leftrightarrow C=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqeq2d.1	$$⊢\phi \to A=B$$
2	1	eqeq1d	$$⊢\phi \to \left(A=C\leftrightarrow B=C\right)$$
3		eqcom	$$⊢C=A\leftrightarrow A=C$$
4		eqcom	$$⊢C=B\leftrightarrow B=C$$
5	2 3 4	3bitr4g	$$⊢\phi \to \left(C=A\leftrightarrow C=B\right)$$