Theorem eqeq2d 2208

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189

This theorem is referenced by:  eqtrd  2229  eq2tri  2256  rspcedeq2vd  2878  rspceeqv  2886  sbceq1g  3104  euabsn  3693  absneu  3695  preq12bg  3804  cbvopab  4105  cbvopab1  4107  cbvopab2  4108  cbvopab1s  4109  cbvopab2v  4111  mpteq12f  4114  cbvmptf  4128  cbvmpt  4129  exmidsssn  4236  exmidsssnc  4237  opth  4271  eqvinop  4277  moop2  4285  euotd  4288  eusvnf  4489  reusv3i  4495  nlimsucg  4603  nn0suc  4641  opelxp  4694  elvvv  4727  relop  4817  elrnmpt1s  4917  elrnmpt1  4918  elsnres  4984  elxp4  5158  elxp5  5159  relresfld  5200  iotajust  5219  iota1  5234  iota2df  5245  funopg  5293  funcnvuni  5328  fun11iun  5528  funcocnv2  5532  nfvres  5595  ssimaex  5625  fvmptg  5640  fvmptdf  5652  fvopab6  5661  fnmptfvd  5669  fmptco  5731  fsng  5738  foco2  5803  elabrex  5807  elabrexg  5808  abrexco  5809  f1veqaeq  5819  dff13f  5820  f1ocnvfv  5829  f1ocnvfvb  5830  fcofo  5834  fliftfun  5846  fliftval  5850  f1oiso2  5877  riota5f  5905  oprabid  5957  rspceov  5968  dfoprab2  5973  mpoeq123dva  5987  mpoeq3dva  5990  cbvoprab1  5998  cbvoprab2  5999  cbvoprab12  6000  cbvmpox  6004  mpomptx  6017  ovmpos  6050  ovmpodf  6058  ovmpodv2  6060  ovi3  6064  ov6g  6065  fnrnov  6073  foov  6074  caovcang  6089  caovcan  6092  f1opw2  6133  opabex3d  6187  opabex3  6188  fo1st  6224  fo2nd  6225  elxp6  6236  op1steq  6246  dfoprab4f  6260  fmpox  6267  fnmpoovd  6282  df1st2  6286  df2nd2  6287  xporderlem  6298  cnvoprab  6301  f1od2  6302  brtpos2  6318  dftpos4  6330  tposfn2  6333  recseq  6373  tfr1onlemaccex  6415  tfrcllemaccex  6428  frecabcl  6466  frecsuc  6474  nna0r  6545  eqerlem  6632  qseq2  6652  ecelqsg  6656  snec  6664  qsinxp  6679  ecoptocl  6690  eroveu  6694  th3qlem1  6705  th3qlem2  6706  th3q  6708  mapsncnv  6763  elixpsn  6803  ixpsnf1o  6804  en1  6867  mapsnen  6879  xpsnen  6889  xpassen  6898  pw2f1odclem  6904  xpf1o  6914  mapen  6916  mapxpen  6918  fidifsnen  6940  ac6sfi  6968  undifdc  6994  djuf1olem  7128  djur  7144  updjud  7157  omp1eomlem  7169  0ct  7182  enumctlemm  7189  fodjuomnilemdc  7219  fodjuomni  7224  fodjumkv  7235  nninfwlporlemd  7247  exmidfodomrlemeldju  7278  exmidfodomrlemreseldju  7279  cc2lem  7349  dfplpq2  7438  dfmpq2  7439  enqbreq2  7441  enq0sym  7516  enq0ref  7517  enq0tr  7518  addnq0mo  7531  mulnq0mo  7532  addnnnq0  7533  mulnnnq0  7534  nqnq0a  7538  nqnq0m  7539  nq0a0  7541  prarloclemcalc  7586  genipv  7593  genpassl  7608  genpassu  7609  addcomprg  7662  mulcomprg  7664  distrlem1prl  7666  distrlem1pru  7667  distrlem5prl  7670  distrlem5pru  7671  1idprl  7674  1idpru  7675  recexprlem1ssl  7717  recexprlem1ssu  7718  addsrmo  7827  mulsrmo  7828  addsrpr  7829  mulsrpr  7830  elreal  7912  axcnre  7965  axcaucvglemval  7981  negeu  8234  subeq0  8269  apreap  8631  apreim  8647  divmulap3  8721  diveqap0  8726  diveqap1  8749  nn0ind-raph  9460  elq  9713  zq  9717  elpq  9740  cnref1o  9742  iccf1o  10096  fzen  10135  fseq1m1p1  10187  fzm1  10192  modqmuladd  10475  modqmuladdnn0  10477  modfzo0difsn  10504  nn0ennn  10542  seqf1oglem1  10628  seq3id2  10635  qsqeqor  10759  bcval5  10872  fihashen1  10908  shftlem  10998  shftfvalg  11000  shftfval  11003  negfi  11410  xrmaxiflemcom  11431  xrnegiso  11444  xrnegcon1d  11446  sumeq2  11541  summodc  11565  fsum3  11569  fsum2dlemstep  11616  isumsplit  11673  mertenslemub  11716  mertensabs  11719  prodeq2w  11738  prodeq2  11739  prodmodc  11760  fprodseq  11765  fprod2dlemstep  11804  moddvds  11981  modm1div  11982  dvdsnegb  11990  dvdsabseq  12029  dvdsmod  12044  odd2np1lem  12054  odd2np1  12055  opeo  12079  omeo  12080  divalglemnn  12100  divalglemeunn  12103  divalglemex  12104  divalglemeuneg  12105  bitsinv1lem  12143  bezoutlemnewy  12188  bezoutlema  12191  bezoutlemb  12192  bezoutlemex  12193  bezoutlemaz  12195  bezoutlembz  12196  eucalglt  12250  qredeq  12289  qredeu  12290  divgcdcoprm0  12294  divgcdcoprmex  12295  cncongr1  12296  cncongr2  12297  qnumdenbi  12385  hashgcdlem  12431  coprimeprodsq2  12452  pythagtriplem18  12475  pythagtriplem19  12476  pceu  12489  pcval  12490  pczpre  12491  pcdiv  12496  dvdsprmpweq  12529  dvdsprmpweqnn  12530  difsqpwdvds  12532  pcmpt  12537  pcfac  12544  oddprmdvds  12548  4sqlem2  12583  4sqlem3  12584  4sqlem4  12586  4sqlem12  12596  evenennn  12635  ennnfonelemim  12666  ptex  12966  intopsn  13069  igsumvalx  13091  gsumfzval  13093  gsumpropd  13094  gsumpropd2  13095  gsumress  13097  gsumval2  13099  ismnddef  13120  sgrpidmndm  13122  mndpfo  13140  mhmex  13164  grpid  13241  grpidrcan  13267  grpidlcan  13268  grplactcnv  13304  isghm  13449  f1ghm0to0  13478  conjghm  13482  srgpcomp  13622  ringadd2  13659  rrgval  13894  opprdomnbg  13906  islmod  13923  lss1d  14015  rspsn  14166  expghmap  14239  zndvds0  14282  znf1o  14283  istopon  14333  eltg3  14377  restsn  14500  txuni2  14576  txopn  14585  upxp  14592  uptx  14594  txrest  14596  hmeoimaf1o  14634  xmettxlem  14829  xmettx  14830  elply2  15055  elplyr  15060  dvdsppwf1o  15309  mpodvdsmulf1o  15310  perfectlem2  15320  perfect  15321  lgslem1  15325  lgsdirnn0  15372  lgsdinn0  15373  gausslemma2dlem0i  15382  gausslemma2dlem1a  15383  gausslemma2d  15394  lgseisenlem2  15396  lgsquadlem2  15403  2lgslem1b  15414  2lgslem3a1  15422  2lgslem3b1  15423  2lgslem3c1  15424  2lgslem3d1  15425  2lgsoddprmlem2  15431  2sqlem2  15440  2sqlem8  15448  2sqlem9  15449  bj-nn0suc0  15680  bj-inf2vnlem1  15700  bj-nn0sucALT  15708  pwle2  15729  iooref1o  15765