Theorem eqeq2d 2364

Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)

Hypothesis

Ref	Expression
eqeq2d.1	⊢ (φ → A = B)

Assertion

Ref	Expression
eqeq2d	⊢ (φ → (C = A ↔ C = B))

Proof of Theorem eqeq2d

Step	Hyp	Ref	Expression
1		eqeq2d.1	. 2 ⊢ (φ → A = B)
2		eqeq2 2362	. 2 ⊢ (A = B → (C = A ↔ C = B))
3	1, 2	syl 15	1 ⊢ (φ → (C = A ↔ C = B))

Syntax hints:   → wi 4   ↔ 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:  eqtrd  2385  eq2tri  2412  sbceq1g  3157  euabsn  3793  absneu  3795  unsneqsn  3888  pwadjoin  4120  preqr2g  4127  preq12bg  4129  snel1c  4141  elpw12  4146  elpw11c  4148  elpw121c  4149  elpw131c  4150  elpw141c  4151  elpw151c  4152  elpw161c  4153  elpw171c  4154  elpw181c  4155  elpw191c  4156  elpw1101c  4157  elpw1111c  4158  pw1sn  4166  opkabssvvk  4209  sikexlem  4296  insklem  4305  pw1equn  4332  pw1eqadj  4333  sspw1  4336  sspw12  4337  iotajust  4339  iota1  4354  iota2df  4366  eladdci  4400  addcid1  4406  nnc0suc  4413  elsuc  4414  elsuci  4415  addcass  4416  nnsucelr  4429  opklefing  4449  opkltfing  4450  lefinaddc  4451  preaddccan2lem1  4455  nulge  4457  leltfintr  4459  ltfintr  4460  ltfinp1  4463  lefinlteq  4464  ltfinex  4465  lefinrflx  4468  ltlefin  4469  eqtfinrelk  4487  tfinltfinlem1  4501  0ceven  4506  sucoddeven  4512  evenodddisjlem1  4516  eventfin  4518  oddtfin  4519  nnadjoin  4521  tfinnn  4535  vfinspsslem1  4551  vfinspss  4552  dfphi2  4570  phi11lem1  4596  0cnelphi  4598  eqvinop  4607  phidisjnn  4616  phialllem1  4617  phialllem2  4618  cbvopab  4631  cbvopab1  4633  cbvopab2  4634  cbvopab1s  4635  cbvopab2v  4637  el1st  4730  elswap  4741  dfid3  4769  br1st  4859  br2nd  4860  brswap2  4861  elsnres  4997  elxp4  5109  dfxp2  5114  funcnvuni  5162  iunfopab  5205  fun11iun  5306  dffn5  5364  fvopab4g  5389  foco2  5427  fsng  5434  fconst5  5456  abrexco  5464  dff13f  5473  f1fveq  5474  f1ocnvfv  5479  f1ocnvfvb  5480  f1oiso2  5501  xpnedisj  5514  oprabid  5551  rspceov  5557  dfoprab2  5559  cbvoprab1  5568  cbvoprab2  5569  cbvoprab12  5570  fnov  5592  ov3  5600  ov6g  5601  fnrnov  5606  foov  5607  caovcan  5629  mpteq12f  5656  mpt2eq123dv  5664  mpt2eq3dva  5670  cbvmpt  5677  cbvmpt2x  5679  mpt2mptx  5709  ovmpt2x  5713  fmpt2x  5731  brtxp  5784  oqelins4  5795  brcrossg  5849  pw1fnf1o  5856  qseq2  5976  ecelqsg  5980  snec  5988  ecoptocl  5997  xpassen  6058  enpw1lem1  6062  enmap2lem3  6066  enmap1lem3  6072  enprmaplem5  6081  enprmapc  6084  1cnc  6140  df1c3g  6142  ncaddccl  6145  ncspw1eu  6160  pw1eltc  6163  el2c  6192  ce2  6193  dflec2  6211  lectr  6212  taddc  6230  tlecg  6231  letc  6232  ce0t  6233  nclenn  6250  csucex  6260  brcsuc  6261  addccan2nclem1  6264  addccan2nclem2  6265  ncslesuc  6268  nmembers1lem1  6269  nmembers1lem3  6271  nncdiv3lem1  6276  nncdiv3lem2  6277  nncdiv3  6278  nnc3n3p1  6279  spaccl  6287  spacind  6288  nchoicelem1  6290  nchoicelem2  6291  nchoicelem3  6292  nchoicelem11  6300  nchoicelem12  6301  nchoicelem16  6305  nchoicelem17  6306  frecsuc  6323