Metamath Proof Explorer


Theorem eqeq2i

Description: Inference from equality to equivalence of equalities. (Contributed by NM, 26-May-1993)

Ref Expression
Hypothesis eqeq2i.1
|- A = B
Assertion eqeq2i
|- ( C = A <-> C = B )

Proof

Step Hyp Ref Expression
1 eqeq2i.1
 |-  A = B
2 eqeq2
 |-  ( A = B -> ( C = A <-> C = B ) )
3 1 2 ax-mp
 |-  ( C = A <-> C = B )