Theorem eqeq2d 2092

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 2090	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

Syntax hints:   → wi 4   ↔ wb 103   = wceq 1284

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 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

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

This theorem is referenced by:  eqtrd  2113  eq2tri  2140  rspcedeq2vd  2710  sbceq1g  2926  euabsn  3462  absneu  3464  preq12bg  3565  cbvopab  3849  cbvopab1  3851  cbvopab2  3852  cbvopab1s  3853  cbvopab2v  3855  mpteq12f  3858  cbvmpt  3872  opth  3992  eqvinop  3998  moop2  4006  euotd  4009  eusvnf  4203  reusv3i  4209  nlimsucg  4309  nn0suc  4345  opelxp  4392  elvvv  4421  relop  4504  elrnmpt1s  4602  elrnmpt1  4603  elsnres  4665  elxp4  4828  elxp5  4829  relresfld  4867  iotajust  4886  iota1  4901  iota2df  4911  funopg  4954  funcnvuni  4988  fun11iun  5167  funcocnv2  5171  nfvres  5227  ssimaex  5255  fvmptg  5269  fvmptdf  5279  fvopab6  5285  foco2  5339  fmptco  5351  fsng  5357  elabrex  5418  abrexco  5419  f1veqaeq  5429  dff13f  5430  f1ocnvfv  5439  f1ocnvfvb  5440  fcofo  5444  fliftfun  5456  fliftval  5460  f1oiso2  5486  riota5f  5512  oprabid  5557  rspceov  5567  dfoprab2  5572  mpt2eq123dva  5586  mpt2eq3dva  5589  cbvoprab1  5596  cbvoprab2  5597  cbvoprab12  5598  cbvmpt2x  5602  mpt2mptx  5615  ovmpt2s  5644  ovmpt2df  5652  ovmpt2dv2  5654  ovi3  5657  ov6g  5658  fnrnov  5666  foov  5667  caovcang  5682  caovcan  5685  f1opw2  5726  opabex3d  5768  opabex3  5769  fo1st  5804  fo2nd  5805  elxp6  5816  op1steq  5825  dfoprab4f  5839  fmpt2x  5846  df1st2  5860  df2nd2  5861  xporderlem  5872  cnvoprab  5875  f1od2  5876  brtpos2  5889  dftpos4  5901  tposfn2  5904  recseq  5944  frecsuc  6014  nna0r  6080  eqerlem  6160  qseq2  6178  ecelqsg  6182  snec  6190  qsinxp  6205  ecoptocl  6216  eroveu  6220  th3qlem1  6231  th3qlem2  6232  th3q  6234  en1  6302  xpsnen  6318  xpassen  6327  fidifsnen  6355  ac6sfi  6379  dfplpq2  6544  dfmpq2  6545  enqbreq2  6547  enq0sym  6622  enq0ref  6623  enq0tr  6624  addnq0mo  6637  mulnq0mo  6638  addnnnq0  6639  mulnnnq0  6640  nqnq0a  6644  nqnq0m  6645  nq0a0  6647  prarloclemcalc  6692  genipv  6699  genpassl  6714  genpassu  6715  addcomprg  6768  mulcomprg  6770  distrlem1prl  6772  distrlem1pru  6773  distrlem5prl  6776  distrlem5pru  6777  1idprl  6780  1idpru  6781  recexprlem1ssl  6823  recexprlem1ssu  6824  addsrmo  6920  mulsrmo  6921  addsrpr  6922  mulsrpr  6923  elreal  6997  axcnre  7047  axcaucvglemval  7063  negeu  7299  subeq0  7334  apreap  7687  apreim  7703  divmulap3  7765  diveqap0  7770  diveqap1  7793  nn0ind-raph  8464  elq  8707  zq  8711  cnref1o  8733  iccf1o  9026  fzen  9062  fseq1m1p1  9112  fzm1  9117  modqmuladd  9368  modqmuladdnn0  9370  modfzo0difsn  9397  nn0ennn  9425  ibcval5  9690  shftlem  9704  shftfvalg  9706  shftfval  9709  negfi  10110  moddvds  10204  dvdsnegb  10212  dvdsabseq  10247  dvdsmod  10262  odd2np1lem  10271  odd2np1  10272  opeo  10297  omeo  10298  divalglemnn  10318  divalglemeunn  10321  divalglemex  10322  divalglemeuneg  10323  bezoutlemnewy  10385  bezoutlema  10388  bezoutlemb  10389  bezoutlemex  10390  bezoutlemaz  10392  bezoutlembz  10393  eucalglt  10439  qredeq  10478  qredeu  10479  divgcdcoprm0  10483  divgcdcoprmex  10484  cncongr1  10485  cncongr2  10486  bj-nn0suc0  10745  bj-inf2vnlem1  10765  bj-nn0sucALT  10773