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  7280  exmidfodomrlemreseldju  7281  cc2lem  7351  dfplpq2  7440  dfmpq2  7441  enqbreq2  7443  enq0sym  7518  enq0ref  7519  enq0tr  7520  addnq0mo  7533  mulnq0mo  7534  addnnnq0  7535  mulnnnq0  7536  nqnq0a  7540  nqnq0m  7541  nq0a0  7543  prarloclemcalc  7588  genipv  7595  genpassl  7610  genpassu  7611  addcomprg  7664  mulcomprg  7666  distrlem1prl  7668  distrlem1pru  7669  distrlem5prl  7672  distrlem5pru  7673  1idprl  7676  1idpru  7677  recexprlem1ssl  7719  recexprlem1ssu  7720  addsrmo  7829  mulsrmo  7830  addsrpr  7831  mulsrpr  7832  elreal  7914  axcnre  7967  axcaucvglemval  7983  negeu  8236  subeq0  8271  apreap  8633  apreim  8649  divmulap3  8723  diveqap0  8728  diveqap1  8751  nn0ind-raph  9462  elq  9715  zq  9719  elpq  9742  cnref1o  9744  iccf1o  10098  fzen  10137  fseq1m1p1  10189  fzm1  10194  modqmuladd  10477  modqmuladdnn0  10479  modfzo0difsn  10506  nn0ennn  10544  seqf1oglem1  10630  seq3id2  10637  qsqeqor  10761  bcval5  10874  fihashen1  10910  shftlem  11000  shftfvalg  11002  shftfval  11005  negfi  11412  xrmaxiflemcom  11433  xrnegiso  11446  xrnegcon1d  11448  sumeq2  11543  summodc  11567  fsum3  11571  fsum2dlemstep  11618  isumsplit  11675  mertenslemub  11718  mertensabs  11721  prodeq2w  11740  prodeq2  11741  prodmodc  11762  fprodseq  11767  fprod2dlemstep  11806  moddvds  11983  modm1div  11984  dvdsnegb  11992  dvdsabseq  12031  dvdsmod  12046  odd2np1lem  12056  odd2np1  12057  opeo  12081  omeo  12082  divalglemnn  12102  divalglemeunn  12105  divalglemex  12106  divalglemeuneg  12107  bitsinv1lem  12145  bezoutlemnewy  12190  bezoutlema  12193  bezoutlemb  12194  bezoutlemex  12195  bezoutlemaz  12197  bezoutlembz  12198  eucalglt  12252  qredeq  12291  qredeu  12292  divgcdcoprm0  12296  divgcdcoprmex  12297  cncongr1  12298  cncongr2  12299  qnumdenbi  12387  hashgcdlem  12433  coprimeprodsq2  12454  pythagtriplem18  12477  pythagtriplem19  12478  pceu  12491  pcval  12492  pczpre  12493  pcdiv  12498  dvdsprmpweq  12531  dvdsprmpweqnn  12532  difsqpwdvds  12534  pcmpt  12539  pcfac  12546  oddprmdvds  12550  4sqlem2  12585  4sqlem3  12586  4sqlem4  12588  4sqlem12  12598  evenennn  12637  ennnfonelemim  12668  ptex  12968  intopsn  13071  igsumvalx  13093  gsumfzval  13095  gsumpropd  13096  gsumpropd2  13097  gsumress  13099  gsumval2  13101  ismnddef  13122  sgrpidmndm  13124  mndpfo  13142  mhmex  13166  grpid  13243  grpidrcan  13269  grpidlcan  13270  grplactcnv  13306  isghm  13451  f1ghm0to0  13480  conjghm  13484  srgpcomp  13624  ringadd2  13661  rrgval  13896  opprdomnbg  13908  islmod  13925  lss1d  14017  rspsn  14168  expghmap  14241  zndvds0  14284  znf1o  14285  mplvalcoe  14324  istopon  14357  eltg3  14401  restsn  14524  txuni2  14600  txopn  14609  upxp  14616  uptx  14618  txrest  14620  hmeoimaf1o  14658  xmettxlem  14853  xmettx  14854  elply2  15079  elplyr  15084  dvdsppwf1o  15333  mpodvdsmulf1o  15334  perfectlem2  15344  perfect  15345  lgslem1  15349  lgsdirnn0  15396  lgsdinn0  15397  gausslemma2dlem0i  15406  gausslemma2dlem1a  15407  gausslemma2d  15418  lgseisenlem2  15420  lgsquadlem2  15427  2lgslem1b  15438  2lgslem3a1  15446  2lgslem3b1  15447  2lgslem3c1  15448  2lgslem3d1  15449  2lgsoddprmlem2  15455  2sqlem2  15464  2sqlem8  15472  2sqlem9  15473  bj-nn0suc0  15704  bj-inf2vnlem1  15724  bj-nn0sucALT  15732  pwle2  15753  iooref1o  15791