Theorem eqeq2d 2177

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  eqtrd  2198  eq2tri  2226  rspcedeq2vd  2840  rspceeqv  2848  sbceq1g  3065  euabsn  3646  absneu  3648  preq12bg  3753  cbvopab  4053  cbvopab1  4055  cbvopab2  4056  cbvopab1s  4057  cbvopab2v  4059  mpteq12f  4062  cbvmptf  4076  cbvmpt  4077  exmidsssn  4181  exmidsssnc  4182  opth  4215  eqvinop  4221  moop2  4229  euotd  4232  eusvnf  4431  reusv3i  4437  nlimsucg  4543  nn0suc  4581  opelxp  4634  elvvv  4667  relop  4754  elrnmpt1s  4854  elrnmpt1  4855  elsnres  4921  elxp4  5091  elxp5  5092  relresfld  5133  iotajust  5152  iota1  5167  iota2df  5177  funopg  5222  funcnvuni  5257  fun11iun  5453  funcocnv2  5457  nfvres  5519  ssimaex  5547  fvmptg  5562  fvmptdf  5573  fvopab6  5582  fmptco  5651  fsng  5658  foco2  5722  elabrex  5726  abrexco  5727  f1veqaeq  5737  dff13f  5738  f1ocnvfv  5747  f1ocnvfvb  5748  fcofo  5752  fliftfun  5764  fliftval  5768  f1oiso2  5795  riota5f  5822  oprabid  5874  rspceov  5884  dfoprab2  5889  mpoeq123dva  5903  mpoeq3dva  5906  cbvoprab1  5914  cbvoprab2  5915  cbvoprab12  5916  cbvmpox  5920  mpomptx  5933  ovmpos  5965  ovmpodf  5973  ovmpodv2  5975  ovi3  5978  ov6g  5979  fnrnov  5987  foov  5988  caovcang  6003  caovcan  6006  f1opw2  6044  opabex3d  6089  opabex3  6090  fo1st  6125  fo2nd  6126  elxp6  6137  op1steq  6147  dfoprab4f  6161  fmpox  6168  fnmpoovd  6183  df1st2  6187  df2nd2  6188  xporderlem  6199  cnvoprab  6202  f1od2  6203  brtpos2  6219  dftpos4  6231  tposfn2  6234  recseq  6274  tfr1onlemaccex  6316  tfrcllemaccex  6329  frecabcl  6367  frecsuc  6375  nna0r  6446  eqerlem  6532  qseq2  6550  ecelqsg  6554  snec  6562  qsinxp  6577  ecoptocl  6588  eroveu  6592  th3qlem1  6603  th3qlem2  6604  th3q  6606  mapsncnv  6661  elixpsn  6701  ixpsnf1o  6702  en1  6765  mapsnen  6777  xpsnen  6787  xpassen  6796  xpf1o  6810  mapen  6812  mapxpen  6814  fidifsnen  6836  ac6sfi  6864  undifdc  6889  djuf1olem  7018  djur  7034  updjud  7047  omp1eomlem  7059  0ct  7072  enumctlemm  7079  fodjuomnilemdc  7108  fodjuomni  7113  fodjumkv  7124  exmidfodomrlemeldju  7155  exmidfodomrlemreseldju  7156  cc2lem  7207  dfplpq2  7295  dfmpq2  7296  enqbreq2  7298  enq0sym  7373  enq0ref  7374  enq0tr  7375  addnq0mo  7388  mulnq0mo  7389  addnnnq0  7390  mulnnnq0  7391  nqnq0a  7395  nqnq0m  7396  nq0a0  7398  prarloclemcalc  7443  genipv  7450  genpassl  7465  genpassu  7466  addcomprg  7519  mulcomprg  7521  distrlem1prl  7523  distrlem1pru  7524  distrlem5prl  7527  distrlem5pru  7528  1idprl  7531  1idpru  7532  recexprlem1ssl  7574  recexprlem1ssu  7575  addsrmo  7684  mulsrmo  7685  addsrpr  7686  mulsrpr  7687  elreal  7769  axcnre  7822  axcaucvglemval  7838  negeu  8089  subeq0  8124  apreap  8485  apreim  8501  divmulap3  8573  diveqap0  8578  diveqap1  8601  nn0ind-raph  9308  elq  9560  zq  9564  elpq  9586  cnref1o  9588  iccf1o  9940  fzen  9978  fseq1m1p1  10030  fzm1  10035  modqmuladd  10301  modqmuladdnn0  10303  modfzo0difsn  10330  nn0ennn  10368  seq3id2  10444  qsqeqor  10565  bcval5  10676  fihashen1  10712  shftlem  10758  shftfvalg  10760  shftfval  10763  negfi  11169  xrmaxiflemcom  11190  xrnegiso  11203  xrnegcon1d  11205  sumeq2  11300  summodc  11324  fsum3  11328  fsum2dlemstep  11375  isumsplit  11432  mertenslemub  11475  mertensabs  11478  prodeq2w  11497  prodeq2  11498  prodmodc  11519  fprodseq  11524  fprod2dlemstep  11563  moddvds  11739  modm1div  11740  dvdsnegb  11748  dvdsabseq  11785  dvdsmod  11800  odd2np1lem  11809  odd2np1  11810  opeo  11834  omeo  11835  divalglemnn  11855  divalglemeunn  11858  divalglemex  11859  divalglemeuneg  11860  bezoutlemnewy  11929  bezoutlema  11932  bezoutlemb  11933  bezoutlemex  11934  bezoutlemaz  11936  bezoutlembz  11937  eucalglt  11989  qredeq  12028  qredeu  12029  divgcdcoprm0  12033  divgcdcoprmex  12034  cncongr1  12035  cncongr2  12036  qnumdenbi  12124  hashgcdlem  12170  coprimeprodsq2  12190  pythagtriplem18  12213  pythagtriplem19  12214  pceu  12227  pcval  12228  pczpre  12229  pcdiv  12234  dvdsprmpweq  12266  dvdsprmpweqnn  12267  difsqpwdvds  12269  pcmpt  12273  pcfac  12280  oddprmdvds  12284  4sqlem2  12319  4sqlem3  12320  4sqlem4  12322  evenennn  12326  ennnfonelemim  12357  intopsn  12598  istopon  12661  eltg3  12707  restsn  12830  txuni2  12906  txopn  12915  upxp  12922  uptx  12924  txrest  12926  hmeoimaf1o  12964  xmettxlem  13159  xmettx  13160  lgslem1  13551  lgsdirnn0  13598  lgsdinn0  13599  2sqlem2  13601  2sqlem8  13609  2sqlem9  13610  bj-nn0suc0  13842  bj-inf2vnlem1  13862  bj-nn0sucALT  13870  pwle2  13888  iooref1o  13923