Theorem eqeq2i 2363

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 2362	. 2 ⊢ (A = B → (C = A ↔ C = B))
3	1, 2	ax-mp 5	1 ⊢ (C = A ↔ C = B)

Syntax hints:   ↔ wb 176   = wceq 1642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346

This theorem is referenced by:  eqtri  2373  rabid2  2789  equncom  3410  ssunpr  3869  sspr  3870  sstp  3871  axprimlem2  4090  preq12b  4128  1cex  4143  dfeu2  4334  dfiota2  4341  dfnnc2  4396  addcid1  4406  addccom  4407  nnc0suc  4413  addcass  4416  nncaddccl  4420  nnsucelrlem1  4425  nndisjeq  4430  preaddccan2lem1  4455  lefinlteq  4464  ltfinex  4465  ltfintri  4467  ltlefin  4469  eqpwrelk  4479  eqtfinrelk  4487  evenodddisjlem1  4516  evenodddisj  4517  srelk  4525  dfphi2  4570  dfop2lem1  4574  dfop2  4576  dfproj12  4577  phialllem1  4617  setconslem1  4732  setconslem2  4733  dfswap2  4742  fnressn  5439  fressnfv  5440  fnov  5592  dffn5v  5707  fnov2  5708  eqerlem  5961  qsid  5991  mapexi  6004  enex  6032  elncs  6120  tcdi  6165  ovcelem1  6172  ceex  6175  nc0suc  6218  muc0or  6253  lecadd2  6267  nnc3p1n3p2  6281  nchoicelem2  6291  nchoicelem17  6306