Theorem eqeq2d 2246

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

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

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  eqtrd  2267  eq2tri  2294  rspcedeq2vd  2934  rspceeqv  2942  sbceq1g  3161  ifeqeqxdc  3673  euabsn  3766  absneu  3768  ifpprsnssdc  3804  preq12bg  3882  cbvopab  4186  cbvopab1  4188  cbvopab2  4189  cbvopab1s  4190  cbvopab2v  4192  mpteq12f  4195  cbvmptf  4209  cbvmpt  4210  exmidsssn  4320  exmidsssnc  4321  opth  4358  eqvinop  4364  moop2  4373  euotd  4376  eusvnf  4579  reusv3i  4585  nlimsucg  4693  nn0suc  4731  opelxp  4784  elvvv  4818  relop  4910  elrnmpt1s  5012  elrnmpt1  5013  elsnres  5080  elxp4  5255  elxp5  5256  relresfld  5297  iotajust  5316  iota1  5332  iota2df  5343  funopg  5391  funcnvuni  5430  fun11iun  5640  funcocnv2  5644  nfvres  5711  ssimaex  5743  fvmptg  5758  fvmptdf  5770  fvopab6  5779  fnmptfvd  5787  fmptco  5848  fsng  5855  fsn2g  5857  funopsn  5865  dfimafnf  5928  foco2  5932  elabrex  5936  elabrexg  5937  abrexco  5938  f1veqaeq  5948  dff13f  5949  f1ocnvfv  5958  f1ocnvfvb  5959  fcofo  5963  fliftfun  5975  fliftval  5979  f1oiso2  6006  riotaeqimp  6036  riota5f  6038  oprabid  6090  rspceov  6101  dfoprab2  6108  mpoeq123dva  6122  mpoeq3dva  6125  cbvoprab1  6133  cbvoprab2  6134  cbvoprab12  6135  cbvmpox  6139  mpomptx  6152  ovmpos  6185  ovmpodf  6193  ovmpodv2  6195  ovi3  6199  ov6g  6200  fnrnov  6208  foov  6209  caovcang  6224  caovcan  6227  f1opw2  6269  opabex3d  6323  opabex3  6324  fo1st  6364  fo2nd  6365  elxp6  6376  op1steq  6386  dfoprab4f  6400  fmpox  6409  fnmpoovd  6424  df1st2  6428  df2nd2  6429  xporderlem  6440  cnvoprab  6443  f1od2  6444  brtpos2  6495  dftpos4  6507  tposfn2  6510  recseq  6550  tfr1onlemaccex  6592  tfrcllemaccex  6605  frecabcl  6643  frecsuc  6651  nna0r  6724  eqerlem  6811  qseq2  6831  ecelqsg  6835  snec  6843  qsinxp  6858  ecoptocl  6869  eroveu  6873  th3qlem1  6884  th3qlem2  6885  th3q  6887  mapsncnv  6943  elixpsn  6983  ixpsnf1o  6984  en1  7052  mapsnend  7065  mapsnen  7066  en2  7078  xpsnen  7085  xpassen  7094  pw2f1odclem  7100  xpf1o  7110  mapen  7112  mapxpen  7114  mapunen  7117  fidifsnen  7138  ac6sfi  7168  undifdc  7197  djuf1olem  7357  djur  7373  updjud  7386  omp1eomlem  7398  0ct  7411  enumctlemm  7418  fodjuomnilemdc  7448  fodjuomni  7453  fodjumkv  7464  nninfwlporlemd  7476  exmidfodomrlemeldju  7515  exmidfodomrlemreseldju  7516  cc2lem  7596  dfplpq2  7685  dfmpq2  7686  enqbreq2  7688  enq0sym  7763  enq0ref  7764  enq0tr  7765  addnq0mo  7778  mulnq0mo  7779  addnnnq0  7780  mulnnnq0  7781  nqnq0a  7785  nqnq0m  7786  nq0a0  7788  prarloclemcalc  7833  genipv  7840  genpassl  7855  genpassu  7856  addcomprg  7909  mulcomprg  7911  distrlem1prl  7913  distrlem1pru  7914  distrlem5prl  7917  distrlem5pru  7918  1idprl  7921  1idpru  7922  recexprlem1ssl  7964  recexprlem1ssu  7965  addsrmo  8074  mulsrmo  8075  addsrpr  8076  mulsrpr  8077  elreal  8159  axcnre  8212  axcaucvglemval  8228  negeu  8480  subeq0  8515  apreap  8878  apreim  8894  divmulap3  8968  diveqap0  8973  diveqap1  8996  nn0ind-raph  9713  elq  9972  zq  9976  elpq  9999  cnref1o  10001  iccf1o  10357  fzen  10397  fseq1m1p1  10451  fzm1  10456  modqmuladd  10752  modqmuladdnn0  10754  modfzo0difsn  10781  nn0ennn  10819  seqf1oglem1  10905  seq3id2  10912  qsqeqor  11036  bcval5  11150  fihashen1  11187  wrdl1exs1  11342  wrdl1s1  11343  wrd2ind  11440  swrdccatin2d  11461  reuccatpfxs1lem  11463  shftlem  11526  shftfvalg  11528  shftfval  11531  negfi  11938  xrmaxiflemcom  11959  xrnegiso  11972  xrnegcon1d  11974  sumeq2  12069  summodc  12094  fsum3  12098  fsum2dlemstep  12145  isumsplit  12202  mertenslemub  12245  mertensabs  12248  prodeq2w  12267  prodeq2  12268  prodmodc  12289  fprodseq  12294  fprod2dlemstep  12333  moddvds  12510  modm1div  12511  dvdsnegb  12519  dvdsabseq  12558  dvdsmod  12573  odd2np1lem  12583  odd2np1  12584  opeo  12608  omeo  12609  divalglemnn  12629  divalglemeunn  12632  divalglemex  12633  divalglemeuneg  12634  bitsinv1lem  12672  bezoutlemnewy  12717  bezoutlema  12720  bezoutlemb  12721  bezoutlemex  12722  bezoutlemaz  12724  bezoutlembz  12725  eucalglt  12779  qredeq  12818  qredeu  12819  divgcdcoprm0  12823  divgcdcoprmex  12824  cncongr1  12825  cncongr2  12826  qnumdenbi  12914  hashgcdlem  12960  coprimeprodsq2  12981  pythagtriplem18  13004  pythagtriplem19  13005  pceu  13018  pcval  13019  pczpre  13020  pcdiv  13025  dvdsprmpweq  13058  dvdsprmpweqnn  13059  difsqpwdvds  13061  pcmpt  13066  pcfac  13073  oddprmdvds  13077  4sqlem2  13112  4sqlem3  13113  4sqlem4  13115  4sqlem12  13125  ballotfilemfc0  13176  ballotfilemfcc  13177  evenennn  13228  ennnfonelemim  13259  ptex  13561  intopsn  13630  igsumvalx  13652  gsumfzval  13654  gsumpropd  13655  gsumpropd2  13656  gsumress  13658  gsumval2  13660  ismnddef  13679  sgrpidmndm  13681  mndpfo  13699  mhmex  13717  grpid  13794  grpidrcan  13820  grpidlcan  13821  grplactcnv  13857  isghm  13996  f1ghm0to0  14025  conjghm  14029  gfsumval  14102  srgpcomp  14233  ringadd2  14270  rrgval  14508  opprdomnbg  14521  islmod  14565  lss1d  14657  rspsn  14808  expghmap  14881  zndvds0  14924  znf1o  14925  psrbagconf1o  14954  mplvalcoe  14971  istopon  15004  eltg3  15048  restsn  15171  txuni2  15247  txopn  15256  upxp  15263  uptx  15265  txrest  15267  hmeoimaf1o  15305  xmettxlem  15500  xmettx  15501  elply2  15726  elplyr  15731  dvdsppwf1o  15983  mpodvdsmulf1o  15984  perfectlem2  15994  perfect  15995  lgslem1  15999  lgsdirnn0  16046  lgsdinn0  16047  gausslemma2dlem0i  16056  gausslemma2dlem1a  16057  gausslemma2d  16068  lgseisenlem2  16070  lgsquadlem2  16077  2lgslem1b  16088  2lgslem3a1  16096  2lgslem3b1  16097  2lgslem3c1  16098  2lgslem3d1  16099  2lgsoddprmlem2  16105  2sqlem2  16114  2sqlem8  16122  2sqlem9  16123  incistruhgr  16211  upgrex  16224  usgredg4  16336  usgredgreu  16337  uspgredg2vtxeu  16339  uspgredg2v  16342  usgredg2vlem2  16344  usgredg2v  16345  vtxdgfifival  16412  vtxdumgrfival  16419  1loopgrvd2fi  16426  wlk1walkdom  16480  upgriswlkdc  16481  eupth2lem3lem3fi  16591  eupth2fi  16600  bj-nn0suc0  16846  bj-inf2vnlem1  16866  bj-nn0sucALT  16874  pwle2  16898  iooref1o  16944  qdiff  16959