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  2788  equncom  3409  ssunpr  3868  sspr  3869  sstp  3870  axprimlem2  4089  preq12b  4127  1cex  4142  dfeu2  4333  dfiota2  4340  dfnnc2  4395  addcid1  4405  addccom  4406  nnc0suc  4412  addcass  4415  nncaddccl  4419  nnsucelrlem1  4424  nndisjeq  4429  preaddccan2lem1  4454  lefinlteq  4463  ltfinex  4464  ltfintri  4466  ltlefin  4468  eqpwrelk  4478  eqtfinrelk  4486  evenodddisjlem1  4515  evenodddisj  4516  srelk  4524  dfphi2  4569  dfop2lem1  4573  dfop2  4575  dfproj12  4576  phialllem1  4616  setconslem1  4731  setconslem2  4732  dfswap2  4741  fnressn  5438  fressnfv  5439  fnov  5591  dffn5v  5706  fnov2  5707  eqerlem  5960  qsid  5990  mapexi  6003  enex  6031  elncs  6119  tcdi  6164  ovcelem1  6171  ceex  6174  nc0suc  6217  muc0or  6252  lecadd2  6266  nnc3p1n3p2  6280  nchoicelem2  6290  nchoicelem17  6305