Theorem eqeq2i 2092

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

Hypothesis

Ref	Expression
eqeq2i.1	|- A = B

Assertion

Ref	Expression
eqeq2i	|- ( C = A <-> C = B )

Proof of Theorem eqeq2i

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

Syntax hints:   <-> wb 103   = wceq 1285

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-cleq 2075

This theorem is referenced by:  eqtri  2102  rabid2  2531  dfss2  2989  equncom  3118  preq12b  3564  preqsn  3569  opeqpr  4010  orddif  4292  dfrel4v  4796  dfiota2  4892  funopg  4958  fnressn  5375  fressnfv  5376  acexmidlemph  5530  fnovim  5634  tpossym  5919  qsid  6230  unfiexmid  6428  recidpirq  7077  axprecex  7097  negeq0  7418  muleqadd  7814  sizeeq0  9807  cjne0  9922  sqrt00  10053  sqrtmsq2i  10148