Theorem equequ2

Description: An equivalence law for equality. (Contributed by NM, 21-Jun-1993) (Proof shortened by Wolf Lammen, 4-Aug-2017) (Proof shortened by BJ, 12-Apr-2021)

	Ref	Expression
Assertion	equequ2	$$⊢x=y\to \left(z=x\leftrightarrow z=y\right)$$

Proof

Step	Hyp	Ref	Expression
1		equtrr	$$⊢x=y\to \left(z=x\to z=y\right)$$
2		equeuclr	$$⊢x=y\to \left(z=y\to z=x\right)$$
3	1 2	impbid	$$⊢x=y\to \left(z=x\leftrightarrow z=y\right)$$