Theorem eqeq2d 2051

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

Hypothesis

Ref	Expression
eqeq2d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
eqeq2d	⊢ (𝜑 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

Proof of Theorem eqeq2d

Step	Hyp	Ref	Expression
1		eqeq2d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqeq2 2049	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

Syntax hints:   → wi 4   ↔ wb 98   = wceq 1243

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  eqtrd  2072  eq2tri  2099  sbceq1g  2870  euabsn  3440  absneu  3442  preq12bg  3544  cbvopab  3828  cbvopab1  3830  cbvopab2  3831  cbvopab1s  3832  cbvopab2v  3834  mpteq12f  3837  cbvmpt  3851  opth  3974  eqvinop  3980  moop2  3988  euotd  3991  eusvnf  4185  reusv3i  4191  nlimsucg  4290  nn0suc  4327  opelxp  4374  elvvv  4403  relop  4486  elrnmpt1s  4584  elrnmpt1  4585  elsnres  4647  elxp4  4808  elxp5  4809  relresfld  4847  iotajust  4866  iota1  4881  iota2df  4891  funopg  4934  funcnvuni  4968  fun11iun  5147  funcocnv2  5151  nfvres  5206  ssimaex  5234  fvmptg  5248  fvmptdf  5258  fvopab6  5264  foco2  5318  fmptco  5330  fsng  5336  elabrex  5397  abrexco  5398  f1veqaeq  5408  dff13f  5409  f1ocnvfv  5419  f1ocnvfvb  5420  fcofo  5424  fliftfun  5436  fliftval  5440  f1oiso2  5466  riota5f  5492  oprabid  5537  rspceov  5547  dfoprab2  5552  mpt2eq123dva  5566  mpt2eq3dva  5569  cbvoprab1  5576  cbvoprab2  5577  cbvoprab12  5578  cbvmpt2x  5582  mpt2mptx  5595  ovmpt2s  5624  ovmpt2df  5632  ovmpt2dv2  5634  ovi3  5637  ov6g  5638  fnrnov  5646  foov  5647  caovcang  5662  caovcan  5665  f1opw2  5706  opabex3d  5748  opabex3  5749  fo1st  5784  fo2nd  5785  elxp6  5796  op1steq  5805  dfoprab4f  5819  fmpt2x  5826  df1st2  5840  df2nd2  5841  xporderlem  5852  brtpos2  5866  dftpos4  5878  tposfn2  5881  recseq  5921  frecsuc  5991  nna0r  6057  eqerlem  6137  qseq2  6155  ecelqsg  6159  snec  6167  qsinxp  6182  ecoptocl  6193  eroveu  6197  th3qlem1  6208  th3qlem2  6209  th3q  6211  en1  6279  xpsnen  6295  xpassen  6304  fidifsnen  6331  ac6sfi  6352  dfplpq2  6452  dfmpq2  6453  enqbreq2  6455  enq0sym  6530  enq0ref  6531  enq0tr  6532  addnq0mo  6545  mulnq0mo  6546  addnnnq0  6547  mulnnnq0  6548  nqnq0a  6552  nqnq0m  6553  nq0a0  6555  prarloclemcalc  6600  genipv  6607  genpassl  6622  genpassu  6623  addcomprg  6676  mulcomprg  6678  distrlem1prl  6680  distrlem1pru  6681  distrlem5prl  6684  distrlem5pru  6685  1idprl  6688  1idpru  6689  recexprlem1ssl  6731  recexprlem1ssu  6732  addsrmo  6828  mulsrmo  6829  addsrpr  6830  mulsrpr  6831  elreal  6905  axcnre  6955  axcaucvglemval  6971  negeu  7202  subeq0  7237  apreap  7578  apreim  7594  divmulap3  7656  diveqap0  7661  diveqap1  7682  nn0ind-raph  8355  elq  8557  zq  8561  cnref1o  8582  iccf1o  8872  fzen  8907  fseq1m1p1  8957  fzm1  8962  nn0ennn  9209  shftlem  9417  shftfvalg  9419  shftfval  9422  bj-nn0suc0  10075  bj-inf2vnlem1  10095  bj-nn0sucALT  10103