Theorem eqeq2d 2111

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1299

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-4 1455  ax-17 1474  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-cleq 2093

This theorem is referenced by:  eqtrd  2132  eq2tri  2159  rspcedeq2vd  2753  rspceeqv  2761  sbceq1g  2973  euabsn  3540  absneu  3542  preq12bg  3647  cbvopab  3939  cbvopab1  3941  cbvopab2  3942  cbvopab1s  3943  cbvopab2v  3945  mpteq12f  3948  cbvmptf  3962  cbvmpt  3963  exmidsssn  4063  exmidsssnc  4064  opth  4097  eqvinop  4103  moop2  4111  euotd  4114  eusvnf  4312  reusv3i  4318  nlimsucg  4419  nn0suc  4456  opelxp  4507  elvvv  4540  relop  4627  elrnmpt1s  4727  elrnmpt1  4728  elsnres  4792  elxp4  4962  elxp5  4963  relresfld  5004  iotajust  5023  iota1  5038  iota2df  5048  funopg  5093  funcnvuni  5128  fun11iun  5322  funcocnv2  5326  nfvres  5386  ssimaex  5414  fvmptg  5429  fvmptdf  5440  fvopab6  5449  fmptco  5518  fsng  5525  foco2  5587  elabrex  5591  abrexco  5592  f1veqaeq  5602  dff13f  5603  f1ocnvfv  5612  f1ocnvfvb  5613  fcofo  5617  fliftfun  5629  fliftval  5633  f1oiso2  5660  riota5f  5686  oprabid  5735  rspceov  5745  dfoprab2  5750  mpoeq123dva  5764  mpoeq3dva  5767  cbvoprab1  5775  cbvoprab2  5776  cbvoprab12  5777  cbvmpox  5781  mpomptx  5794  ovmpos  5826  ovmpodf  5834  ovmpodv2  5836  ovi3  5839  ov6g  5840  fnrnov  5848  foov  5849  caovcang  5864  caovcan  5867  f1opw2  5908  opabex3d  5950  opabex3  5951  fo1st  5986  fo2nd  5987  elxp6  5998  op1steq  6007  dfoprab4f  6021  fmpox  6028  fnmpoovd  6042  df1st2  6046  df2nd2  6047  xporderlem  6058  cnvoprab  6061  f1od2  6062  brtpos2  6078  dftpos4  6090  tposfn2  6093  recseq  6133  tfr1onlemaccex  6175  tfrcllemaccex  6188  frecabcl  6226  frecsuc  6234  nna0r  6304  eqerlem  6390  qseq2  6408  ecelqsg  6412  snec  6420  qsinxp  6435  ecoptocl  6446  eroveu  6450  th3qlem1  6461  th3qlem2  6462  th3q  6464  mapsncnv  6519  elixpsn  6559  ixpsnf1o  6560  en1  6623  mapsnen  6635  xpsnen  6644  xpassen  6653  xpf1o  6667  mapen  6669  mapxpen  6671  fidifsnen  6693  ac6sfi  6721  undifdc  6741  djuf1olem  6853  djur  6869  updjud  6882  omp1eomlem  6894  0ct  6907  enumctlemm  6913  fodjuomnilemdc  6928  fodjuomni  6933  fodjumkv  6945  exmidfodomrlemeldju  6964  exmidfodomrlemreseldju  6965  dfplpq2  7063  dfmpq2  7064  enqbreq2  7066  enq0sym  7141  enq0ref  7142  enq0tr  7143  addnq0mo  7156  mulnq0mo  7157  addnnnq0  7158  mulnnnq0  7159  nqnq0a  7163  nqnq0m  7164  nq0a0  7166  prarloclemcalc  7211  genipv  7218  genpassl  7233  genpassu  7234  addcomprg  7287  mulcomprg  7289  distrlem1prl  7291  distrlem1pru  7292  distrlem5prl  7295  distrlem5pru  7296  1idprl  7299  1idpru  7300  recexprlem1ssl  7342  recexprlem1ssu  7343  addsrmo  7439  mulsrmo  7440  addsrpr  7441  mulsrpr  7442  elreal  7516  axcnre  7566  axcaucvglemval  7582  negeu  7824  subeq0  7859  apreap  8215  apreim  8231  divmulap3  8298  diveqap0  8303  diveqap1  8326  nn0ind-raph  9020  elq  9264  zq  9268  cnref1o  9290  iccf1o  9628  fzen  9664  fseq1m1p1  9716  fzm1  9721  modqmuladd  9980  modqmuladdnn0  9982  modfzo0difsn  10009  nn0ennn  10047  seq3id2  10123  bcval5  10350  fihashen1  10386  shftlem  10429  shftfvalg  10431  shftfval  10434  negfi  10838  xrmaxiflemcom  10857  xrnegiso  10870  xrnegcon1d  10872  sumeq2  10967  summodc  10991  fsum3  10995  fsum2dlemstep  11042  isumsplit  11099  mertenslemub  11142  mertensabs  11145  moddvds  11297  dvdsnegb  11305  dvdsabseq  11340  dvdsmod  11355  odd2np1lem  11364  odd2np1  11365  opeo  11389  omeo  11390  divalglemnn  11410  divalglemeunn  11413  divalglemex  11414  divalglemeuneg  11415  bezoutlemnewy  11477  bezoutlema  11480  bezoutlemb  11481  bezoutlemex  11482  bezoutlemaz  11484  bezoutlembz  11485  eucalglt  11531  qredeq  11570  qredeu  11571  divgcdcoprm0  11575  divgcdcoprmex  11576  cncongr1  11577  cncongr2  11578  qnumdenbi  11662  hashgcdlem  11695  evenennn  11698  ennnfonelemim  11729  istopon  11962  eltg3  12008  restsn  12131  txuni2  12206  txopn  12215  upxp  12222  uptx  12224  txrest  12226  bj-nn0suc0  12733  bj-inf2vnlem1  12753  bj-nn0sucALT  12761  pwle2  12779