Metamath Proof Explorer
Description: Equality implies equivalence of equalities. (Contributed by NM, 26May1993) (Proof shortened by Wolf Lammen, 19Nov2019)


Ref 
Expression 

Assertion 
eqeq2 
$${\u22a2}{A}={B}\to \left({C}={A}\leftrightarrow {C}={B}\right)$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

id 
$${\u22a2}{A}={B}\to {A}={B}$$ 
2 
1

eqeq2d 
$${\u22a2}{A}={B}\to \left({C}={A}\leftrightarrow {C}={B}\right)$$ 