Theorem eqeq2d 2201

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 2199	. 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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171

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

This theorem is referenced by:  eqtrd  2222  eq2tri  2249  rspcedeq2vd  2866  rspceeqv  2874  sbceq1g  3092  euabsn  3677  absneu  3679  preq12bg  3788  cbvopab  4089  cbvopab1  4091  cbvopab2  4092  cbvopab1s  4093  cbvopab2v  4095  mpteq12f  4098  cbvmptf  4112  cbvmpt  4113  exmidsssn  4220  exmidsssnc  4221  opth  4255  eqvinop  4261  moop2  4269  euotd  4272  eusvnf  4471  reusv3i  4477  nlimsucg  4583  nn0suc  4621  opelxp  4674  elvvv  4707  relop  4795  elrnmpt1s  4895  elrnmpt1  4896  elsnres  4962  elxp4  5134  elxp5  5135  relresfld  5176  iotajust  5195  iota1  5210  iota2df  5221  funopg  5269  funcnvuni  5304  fun11iun  5501  funcocnv2  5505  nfvres  5567  ssimaex  5597  fvmptg  5612  fvmptdf  5623  fvopab6  5632  fnmptfvd  5640  fmptco  5702  fsng  5709  foco2  5774  elabrex  5778  elabrexg  5779  abrexco  5780  f1veqaeq  5790  dff13f  5791  f1ocnvfv  5800  f1ocnvfvb  5801  fcofo  5805  fliftfun  5817  fliftval  5821  f1oiso2  5848  riota5f  5875  oprabid  5927  rspceov  5937  dfoprab2  5942  mpoeq123dva  5956  mpoeq3dva  5959  cbvoprab1  5967  cbvoprab2  5968  cbvoprab12  5969  cbvmpox  5973  mpomptx  5986  ovmpos  6019  ovmpodf  6027  ovmpodv2  6029  ovi3  6032  ov6g  6033  fnrnov  6041  foov  6042  caovcang  6057  caovcan  6060  f1opw2  6099  opabex3d  6145  opabex3  6146  fo1st  6181  fo2nd  6182  elxp6  6193  op1steq  6203  dfoprab4f  6217  fmpox  6224  fnmpoovd  6239  df1st2  6243  df2nd2  6244  xporderlem  6255  cnvoprab  6258  f1od2  6259  brtpos2  6275  dftpos4  6287  tposfn2  6290  recseq  6330  tfr1onlemaccex  6372  tfrcllemaccex  6385  frecabcl  6423  frecsuc  6431  nna0r  6502  eqerlem  6589  qseq2  6609  ecelqsg  6613  snec  6621  qsinxp  6636  ecoptocl  6647  eroveu  6651  th3qlem1  6662  th3qlem2  6663  th3q  6665  mapsncnv  6720  elixpsn  6760  ixpsnf1o  6761  en1  6824  mapsnen  6836  xpsnen  6846  xpassen  6855  pw2f1odclem  6861  xpf1o  6871  mapen  6873  mapxpen  6875  fidifsnen  6897  ac6sfi  6925  undifdc  6951  djuf1olem  7081  djur  7097  updjud  7110  omp1eomlem  7122  0ct  7135  enumctlemm  7142  fodjuomnilemdc  7171  fodjuomni  7176  fodjumkv  7187  nninfwlporlemd  7199  exmidfodomrlemeldju  7227  exmidfodomrlemreseldju  7228  cc2lem  7294  dfplpq2  7382  dfmpq2  7383  enqbreq2  7385  enq0sym  7460  enq0ref  7461  enq0tr  7462  addnq0mo  7475  mulnq0mo  7476  addnnnq0  7477  mulnnnq0  7478  nqnq0a  7482  nqnq0m  7483  nq0a0  7485  prarloclemcalc  7530  genipv  7537  genpassl  7552  genpassu  7553  addcomprg  7606  mulcomprg  7608  distrlem1prl  7610  distrlem1pru  7611  distrlem5prl  7614  distrlem5pru  7615  1idprl  7618  1idpru  7619  recexprlem1ssl  7661  recexprlem1ssu  7662  addsrmo  7771  mulsrmo  7772  addsrpr  7773  mulsrpr  7774  elreal  7856  axcnre  7909  axcaucvglemval  7925  negeu  8177  subeq0  8212  apreap  8573  apreim  8589  divmulap3  8663  diveqap0  8668  diveqap1  8691  nn0ind-raph  9399  elq  9651  zq  9655  elpq  9677  cnref1o  9679  iccf1o  10033  fzen  10072  fseq1m1p1  10124  fzm1  10129  modqmuladd  10396  modqmuladdnn0  10398  modfzo0difsn  10425  nn0ennn  10463  seq3id2  10539  qsqeqor  10661  bcval5  10774  fihashen1  10810  shftlem  10856  shftfvalg  10858  shftfval  10861  negfi  11267  xrmaxiflemcom  11288  xrnegiso  11301  xrnegcon1d  11303  sumeq2  11398  summodc  11422  fsum3  11426  fsum2dlemstep  11473  isumsplit  11530  mertenslemub  11573  mertensabs  11576  prodeq2w  11595  prodeq2  11596  prodmodc  11617  fprodseq  11622  fprod2dlemstep  11661  moddvds  11837  modm1div  11838  dvdsnegb  11846  dvdsabseq  11884  dvdsmod  11899  odd2np1lem  11908  odd2np1  11909  opeo  11933  omeo  11934  divalglemnn  11954  divalglemeunn  11957  divalglemex  11958  divalglemeuneg  11959  bezoutlemnewy  12028  bezoutlema  12031  bezoutlemb  12032  bezoutlemex  12033  bezoutlemaz  12035  bezoutlembz  12036  eucalglt  12088  qredeq  12127  qredeu  12128  divgcdcoprm0  12132  divgcdcoprmex  12133  cncongr1  12134  cncongr2  12135  qnumdenbi  12223  hashgcdlem  12269  coprimeprodsq2  12289  pythagtriplem18  12312  pythagtriplem19  12313  pceu  12326  pcval  12327  pczpre  12328  pcdiv  12333  dvdsprmpweq  12366  dvdsprmpweqnn  12367  difsqpwdvds  12369  pcmpt  12374  pcfac  12381  oddprmdvds  12385  4sqlem2  12420  4sqlem3  12421  4sqlem4  12423  4sqlem12  12433  evenennn  12443  ennnfonelemim  12474  ptex  12766  intopsn  12840  ismnddef  12876  sgrpidmndm  12878  mndpfo  12896  mhmex  12911  grpid  12980  grpidrcan  13006  grpidlcan  13007  grplactcnv  13043  isghm  13179  f1ghm0to0  13208  conjghm  13212  srgpcomp  13341  ringadd2  13378  islmod  13604  lss1d  13696  istopon  13965  eltg3  14009  restsn  14132  txuni2  14208  txopn  14217  upxp  14224  uptx  14226  txrest  14228  hmeoimaf1o  14266  xmettxlem  14461  xmettx  14462  lgslem1  14854  lgsdirnn0  14901  lgsdinn0  14902  lgseisenlem2  14904  2lgsoddprmlem2  14907  2sqlem2  14915  2sqlem8  14923  2sqlem9  14924  bj-nn0suc0  15155  bj-inf2vnlem1  15175  bj-nn0sucALT  15183  pwle2  15202  iooref1o  15236