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 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  eqtrd  2264  eq2tri  2291  rspcedeq2vd  2920  rspceeqv  2928  sbceq1g  3147  euabsn  3741  absneu  3743  ifpprsnssdc  3779  preq12bg  3856  cbvopab  4160  cbvopab1  4162  cbvopab2  4163  cbvopab1s  4164  cbvopab2v  4166  mpteq12f  4169  cbvmptf  4183  cbvmpt  4184  exmidsssn  4292  exmidsssnc  4293  opth  4329  eqvinop  4335  moop2  4344  euotd  4347  eusvnf  4550  reusv3i  4556  nlimsucg  4664  nn0suc  4702  opelxp  4755  elvvv  4789  relop  4880  elrnmpt1s  4982  elrnmpt1  4983  elsnres  5050  elxp4  5224  elxp5  5225  relresfld  5266  iotajust  5285  iota1  5301  iota2df  5312  funopg  5360  funcnvuni  5399  fun11iun  5604  funcocnv2  5608  nfvres  5675  ssimaex  5707  fvmptg  5722  fvmptdf  5734  fvopab6  5743  fnmptfvd  5751  fmptco  5813  fsng  5820  fsn2g  5822  funopsn  5830  foco2  5894  elabrex  5898  elabrexg  5899  abrexco  5900  f1veqaeq  5910  dff13f  5911  f1ocnvfv  5920  f1ocnvfvb  5921  fcofo  5925  fliftfun  5937  fliftval  5941  f1oiso2  5968  riotaeqimp  5996  riota5f  5998  oprabid  6050  rspceov  6061  dfoprab2  6068  mpoeq123dva  6082  mpoeq3dva  6085  cbvoprab1  6093  cbvoprab2  6094  cbvoprab12  6095  cbvmpox  6099  mpomptx  6112  ovmpos  6145  ovmpodf  6153  ovmpodv2  6155  ovi3  6159  ov6g  6160  fnrnov  6168  foov  6169  caovcang  6184  caovcan  6187  f1opw2  6229  opabex3d  6283  opabex3  6284  fo1st  6320  fo2nd  6321  elxp6  6332  op1steq  6342  dfoprab4f  6356  fmpox  6365  fnmpoovd  6380  df1st2  6384  df2nd2  6385  xporderlem  6396  cnvoprab  6399  f1od2  6400  brtpos2  6417  dftpos4  6429  tposfn2  6432  recseq  6472  tfr1onlemaccex  6514  tfrcllemaccex  6527  frecabcl  6565  frecsuc  6573  nna0r  6646  eqerlem  6733  qseq2  6753  ecelqsg  6757  snec  6765  qsinxp  6780  ecoptocl  6791  eroveu  6795  th3qlem1  6806  th3qlem2  6807  th3q  6809  mapsncnv  6864  elixpsn  6904  ixpsnf1o  6905  en1  6973  mapsnen  6986  en2  6998  xpsnen  7005  xpassen  7014  pw2f1odclem  7020  xpf1o  7030  mapen  7032  mapxpen  7034  fidifsnen  7057  ac6sfi  7087  undifdc  7116  djuf1olem  7252  djur  7268  updjud  7281  omp1eomlem  7293  0ct  7306  enumctlemm  7313  fodjuomnilemdc  7343  fodjuomni  7348  fodjumkv  7359  nninfwlporlemd  7371  exmidfodomrlemeldju  7410  exmidfodomrlemreseldju  7411  cc2lem  7485  dfplpq2  7574  dfmpq2  7575  enqbreq2  7577  enq0sym  7652  enq0ref  7653  enq0tr  7654  addnq0mo  7667  mulnq0mo  7668  addnnnq0  7669  mulnnnq0  7670  nqnq0a  7674  nqnq0m  7675  nq0a0  7677  prarloclemcalc  7722  genipv  7729  genpassl  7744  genpassu  7745  addcomprg  7798  mulcomprg  7800  distrlem1prl  7802  distrlem1pru  7803  distrlem5prl  7806  distrlem5pru  7807  1idprl  7810  1idpru  7811  recexprlem1ssl  7853  recexprlem1ssu  7854  addsrmo  7963  mulsrmo  7964  addsrpr  7965  mulsrpr  7966  elreal  8048  axcnre  8101  axcaucvglemval  8117  negeu  8370  subeq0  8405  apreap  8767  apreim  8783  divmulap3  8857  diveqap0  8862  diveqap1  8885  nn0ind-raph  9597  elq  9856  zq  9860  elpq  9883  cnref1o  9885  iccf1o  10239  fzen  10278  fseq1m1p1  10330  fzm1  10335  modqmuladd  10629  modqmuladdnn0  10631  modfzo0difsn  10658  nn0ennn  10696  seqf1oglem1  10782  seq3id2  10789  qsqeqor  10913  bcval5  11026  fihashen1  11062  wrdl1exs1  11210  wrdl1s1  11211  wrd2ind  11308  swrdccatin2d  11329  reuccatpfxs1lem  11331  shftlem  11381  shftfvalg  11383  shftfval  11386  negfi  11793  xrmaxiflemcom  11814  xrnegiso  11827  xrnegcon1d  11829  sumeq2  11924  summodc  11949  fsum3  11953  fsum2dlemstep  12000  isumsplit  12057  mertenslemub  12100  mertensabs  12103  prodeq2w  12122  prodeq2  12123  prodmodc  12144  fprodseq  12149  fprod2dlemstep  12188  moddvds  12365  modm1div  12366  dvdsnegb  12374  dvdsabseq  12413  dvdsmod  12428  odd2np1lem  12438  odd2np1  12439  opeo  12463  omeo  12464  divalglemnn  12484  divalglemeunn  12487  divalglemex  12488  divalglemeuneg  12489  bitsinv1lem  12527  bezoutlemnewy  12572  bezoutlema  12575  bezoutlemb  12576  bezoutlemex  12577  bezoutlemaz  12579  bezoutlembz  12580  eucalglt  12634  qredeq  12673  qredeu  12674  divgcdcoprm0  12678  divgcdcoprmex  12679  cncongr1  12680  cncongr2  12681  qnumdenbi  12769  hashgcdlem  12815  coprimeprodsq2  12836  pythagtriplem18  12859  pythagtriplem19  12860  pceu  12873  pcval  12874  pczpre  12875  pcdiv  12880  dvdsprmpweq  12913  dvdsprmpweqnn  12914  difsqpwdvds  12916  pcmpt  12921  pcfac  12928  oddprmdvds  12932  4sqlem2  12967  4sqlem3  12968  4sqlem4  12970  4sqlem12  12980  evenennn  13019  ennnfonelemim  13050  ptex  13352  intopsn  13455  igsumvalx  13477  gsumfzval  13479  gsumpropd  13480  gsumpropd2  13481  gsumress  13483  gsumval2  13485  ismnddef  13506  sgrpidmndm  13508  mndpfo  13526  mhmex  13550  grpid  13627  grpidrcan  13653  grpidlcan  13654  grplactcnv  13690  isghm  13835  f1ghm0to0  13864  conjghm  13868  srgpcomp  14009  ringadd2  14046  rrgval  14282  opprdomnbg  14294  islmod  14311  lss1d  14403  rspsn  14554  expghmap  14627  zndvds0  14670  znf1o  14671  mplvalcoe  14710  istopon  14743  eltg3  14787  restsn  14910  txuni2  14986  txopn  14995  upxp  15002  uptx  15004  txrest  15006  hmeoimaf1o  15044  xmettxlem  15239  xmettx  15240  elply2  15465  elplyr  15470  dvdsppwf1o  15719  mpodvdsmulf1o  15720  perfectlem2  15730  perfect  15731  lgslem1  15735  lgsdirnn0  15782  lgsdinn0  15783  gausslemma2dlem0i  15792  gausslemma2dlem1a  15793  gausslemma2d  15804  lgseisenlem2  15806  lgsquadlem2  15813  2lgslem1b  15824  2lgslem3a1  15832  2lgslem3b1  15833  2lgslem3c1  15834  2lgslem3d1  15835  2lgsoddprmlem2  15841  2sqlem2  15850  2sqlem8  15858  2sqlem9  15859  incistruhgr  15947  upgrex  15960  usgredg4  16072  usgredgreu  16073  uspgredg2vtxeu  16075  uspgredg2v  16078  usgredg2vlem2  16080  usgredg2v  16081  vtxdgfifival  16148  vtxdumgrfival  16155  1loopgrvd2fi  16162  wlk1walkdom  16216  upgriswlkdc  16217  eupth2lem3lem3fi  16327  eupth2fi  16336  bj-nn0suc0  16571  bj-inf2vnlem1  16591  bj-nn0sucALT  16599  pwle2  16625  iooref1o  16664  qdiff  16679  gfsumval  16707