Theorem eqeq2d 2243

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 2241	. 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 2213

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

This theorem is referenced by:  eqtrd  2264  eq2tri  2291  rspcedeq2vd  2921  rspceeqv  2929  sbceq1g  3148  euabsn  3745  absneu  3747  ifpprsnssdc  3783  preq12bg  3861  cbvopab  4165  cbvopab1  4167  cbvopab2  4168  cbvopab1s  4169  cbvopab2v  4171  mpteq12f  4174  cbvmptf  4188  cbvmpt  4189  exmidsssn  4298  exmidsssnc  4299  opth  4335  eqvinop  4341  moop2  4350  euotd  4353  eusvnf  4556  reusv3i  4562  nlimsucg  4670  nn0suc  4708  opelxp  4761  elvvv  4795  relop  4886  elrnmpt1s  4988  elrnmpt1  4989  elsnres  5056  elxp4  5231  elxp5  5232  relresfld  5273  iotajust  5292  iota1  5308  iota2df  5319  funopg  5367  funcnvuni  5406  fun11iun  5613  funcocnv2  5617  nfvres  5684  ssimaex  5716  fvmptg  5731  fvmptdf  5743  fvopab6  5752  fnmptfvd  5760  fmptco  5821  fsng  5828  fsn2g  5830  funopsn  5838  foco2  5904  elabrex  5908  elabrexg  5909  abrexco  5910  f1veqaeq  5920  dff13f  5921  f1ocnvfv  5930  f1ocnvfvb  5931  fcofo  5935  fliftfun  5947  fliftval  5951  f1oiso2  5978  riotaeqimp  6006  riota5f  6008  oprabid  6060  rspceov  6071  dfoprab2  6078  mpoeq123dva  6092  mpoeq3dva  6095  cbvoprab1  6103  cbvoprab2  6104  cbvoprab12  6105  cbvmpox  6109  mpomptx  6122  ovmpos  6155  ovmpodf  6163  ovmpodv2  6165  ovi3  6169  ov6g  6170  fnrnov  6178  foov  6179  caovcang  6194  caovcan  6197  f1opw2  6239  opabex3d  6292  opabex3  6293  fo1st  6329  fo2nd  6330  elxp6  6341  op1steq  6351  dfoprab4f  6365  fmpox  6374  fnmpoovd  6389  df1st2  6393  df2nd2  6394  xporderlem  6405  cnvoprab  6408  f1od2  6409  brtpos2  6460  dftpos4  6472  tposfn2  6475  recseq  6515  tfr1onlemaccex  6557  tfrcllemaccex  6570  frecabcl  6608  frecsuc  6616  nna0r  6689  eqerlem  6776  qseq2  6796  ecelqsg  6800  snec  6808  qsinxp  6823  ecoptocl  6834  eroveu  6838  th3qlem1  6849  th3qlem2  6850  th3q  6852  mapsncnv  6907  elixpsn  6947  ixpsnf1o  6948  en1  7016  mapsnen  7029  en2  7041  xpsnen  7048  xpassen  7057  pw2f1odclem  7063  xpf1o  7073  mapen  7075  mapxpen  7077  fidifsnen  7100  ac6sfi  7130  undifdc  7159  djuf1olem  7295  djur  7311  updjud  7324  omp1eomlem  7336  0ct  7349  enumctlemm  7356  fodjuomnilemdc  7386  fodjuomni  7391  fodjumkv  7402  nninfwlporlemd  7414  exmidfodomrlemeldju  7453  exmidfodomrlemreseldju  7454  cc2lem  7528  dfplpq2  7617  dfmpq2  7618  enqbreq2  7620  enq0sym  7695  enq0ref  7696  enq0tr  7697  addnq0mo  7710  mulnq0mo  7711  addnnnq0  7712  mulnnnq0  7713  nqnq0a  7717  nqnq0m  7718  nq0a0  7720  prarloclemcalc  7765  genipv  7772  genpassl  7787  genpassu  7788  addcomprg  7841  mulcomprg  7843  distrlem1prl  7845  distrlem1pru  7846  distrlem5prl  7849  distrlem5pru  7850  1idprl  7853  1idpru  7854  recexprlem1ssl  7896  recexprlem1ssu  7897  addsrmo  8006  mulsrmo  8007  addsrpr  8008  mulsrpr  8009  elreal  8091  axcnre  8144  axcaucvglemval  8160  negeu  8412  subeq0  8447  apreap  8809  apreim  8825  divmulap3  8899  diveqap0  8904  diveqap1  8927  nn0ind-raph  9641  elq  9900  zq  9904  elpq  9927  cnref1o  9929  iccf1o  10284  fzen  10323  fseq1m1p1  10375  fzm1  10380  modqmuladd  10674  modqmuladdnn0  10676  modfzo0difsn  10703  nn0ennn  10741  seqf1oglem1  10827  seq3id2  10834  qsqeqor  10958  bcval5  11071  fihashen1  11107  wrdl1exs1  11255  wrdl1s1  11256  wrd2ind  11353  swrdccatin2d  11374  reuccatpfxs1lem  11376  shftlem  11439  shftfvalg  11441  shftfval  11444  negfi  11851  xrmaxiflemcom  11872  xrnegiso  11885  xrnegcon1d  11887  sumeq2  11982  summodc  12007  fsum3  12011  fsum2dlemstep  12058  isumsplit  12115  mertenslemub  12158  mertensabs  12161  prodeq2w  12180  prodeq2  12181  prodmodc  12202  fprodseq  12207  fprod2dlemstep  12246  moddvds  12423  modm1div  12424  dvdsnegb  12432  dvdsabseq  12471  dvdsmod  12486  odd2np1lem  12496  odd2np1  12497  opeo  12521  omeo  12522  divalglemnn  12542  divalglemeunn  12545  divalglemex  12546  divalglemeuneg  12547  bitsinv1lem  12585  bezoutlemnewy  12630  bezoutlema  12633  bezoutlemb  12634  bezoutlemex  12635  bezoutlemaz  12637  bezoutlembz  12638  eucalglt  12692  qredeq  12731  qredeu  12732  divgcdcoprm0  12736  divgcdcoprmex  12737  cncongr1  12738  cncongr2  12739  qnumdenbi  12827  hashgcdlem  12873  coprimeprodsq2  12894  pythagtriplem18  12917  pythagtriplem19  12918  pceu  12931  pcval  12932  pczpre  12933  pcdiv  12938  dvdsprmpweq  12971  dvdsprmpweqnn  12972  difsqpwdvds  12974  pcmpt  12979  pcfac  12986  oddprmdvds  12990  4sqlem2  13025  4sqlem3  13026  4sqlem4  13028  4sqlem12  13038  evenennn  13077  ennnfonelemim  13108  ptex  13410  intopsn  13513  igsumvalx  13535  gsumfzval  13537  gsumpropd  13538  gsumpropd2  13539  gsumress  13541  gsumval2  13543  ismnddef  13564  sgrpidmndm  13566  mndpfo  13584  mhmex  13608  grpid  13685  grpidrcan  13711  grpidlcan  13712  grplactcnv  13748  isghm  13893  f1ghm0to0  13922  conjghm  13926  srgpcomp  14067  ringadd2  14104  rrgval  14340  opprdomnbg  14353  islmod  14370  lss1d  14462  rspsn  14613  expghmap  14686  zndvds0  14729  znf1o  14730  psrbagconf1o  14757  mplvalcoe  14774  istopon  14807  eltg3  14851  restsn  14974  txuni2  15050  txopn  15059  upxp  15066  uptx  15068  txrest  15070  hmeoimaf1o  15108  xmettxlem  15303  xmettx  15304  elply2  15529  elplyr  15534  dvdsppwf1o  15786  mpodvdsmulf1o  15787  perfectlem2  15797  perfect  15798  lgslem1  15802  lgsdirnn0  15849  lgsdinn0  15850  gausslemma2dlem0i  15859  gausslemma2dlem1a  15860  gausslemma2d  15871  lgseisenlem2  15873  lgsquadlem2  15880  2lgslem1b  15891  2lgslem3a1  15899  2lgslem3b1  15900  2lgslem3c1  15901  2lgslem3d1  15902  2lgsoddprmlem2  15908  2sqlem2  15917  2sqlem8  15925  2sqlem9  15926  incistruhgr  16014  upgrex  16027  usgredg4  16139  usgredgreu  16140  uspgredg2vtxeu  16142  uspgredg2v  16145  usgredg2vlem2  16147  usgredg2v  16148  vtxdgfifival  16215  vtxdumgrfival  16222  1loopgrvd2fi  16229  wlk1walkdom  16283  upgriswlkdc  16284  eupth2lem3lem3fi  16394  eupth2fi  16403  bj-nn0suc0  16649  bj-inf2vnlem1  16669  bj-nn0sucALT  16677  pwle2  16703  iooref1o  16749  qdiff  16764  gfsumval  16792