Theorem eqeq2d 2250

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqtrd  2271  eq2tri  2298  rspcedeq2vd  2940  rspceeqv  2948  sbceq1g  3167  ifeqeqxdc  3687  euabsn  3781  absneu  3783  ifpprsnssdc  3820  preq12bg  3898  cbvopab  4202  cbvopab1  4204  cbvopab2  4205  cbvopab1s  4206  cbvopab2v  4208  mpteq12f  4211  cbvmptf  4225  cbvmpt  4226  exmidsssn  4339  exmidsssnc  4340  opth  4377  eqvinop  4383  moop2  4392  euotd  4395  eusvnf  4599  reusv3i  4605  nlimsucg  4713  nn0suc  4751  opelxp  4804  elvvv  4838  relop  4930  elrnmpt1s  5032  elrnmpt1  5033  elsnres  5100  elxp4  5275  elxp5  5276  relresfld  5317  iotajust  5336  iota1  5352  iota2df  5363  funopg  5411  funcnvuni  5450  fun11iun  5660  funcocnv2  5664  nfvres  5732  ssimaex  5764  fvmptg  5781  fvmptdf  5793  fvopab6  5805  fnmptfvd  5813  fmptco  5874  fsng  5881  fsn2g  5883  funopsn  5891  dfimafnf  5955  foco2  5959  elabrex  5963  elabrexg  5964  abrexco  5965  f1veqaeq  5975  dff13f  5976  f1ocnvfv  5985  f1ocnvfvb  5986  fcofo  5990  fliftfun  6002  fliftval  6006  f1oiso2  6033  riotaeqimp  6063  riota5f  6065  oprabid  6117  rspceov  6128  dfoprab2  6135  mpoeq123dva  6149  mpoeq3dva  6152  cbvoprab1  6160  cbvoprab2  6161  cbvoprab12  6162  cbvmpox  6166  mpomptx  6179  ovmpos  6212  ovmpodf  6220  ovmpodv2  6222  ovi3  6226  ov6g  6227  fnrnov  6235  foov  6236  caovcang  6251  caovcan  6254  f1opw2  6296  opabex3d  6350  opabex3  6351  fo1st  6391  fo2nd  6392  elxp6  6403  op1steq  6413  dfoprab4f  6427  fmpox  6436  fnmpoovd  6451  df1st2  6455  df2nd2  6456  xporderlem  6467  cnvoprab  6470  f1od2  6471  brtpos2  6522  dftpos4  6534  tposfn2  6537  recseq  6577  tfr1onlemaccex  6619  tfrcllemaccex  6632  frecabcl  6670  frecsuc  6678  nna0r  6751  eqerlem  6838  qseq2  6858  ecelqsg  6862  snec  6870  qsinxp  6885  ecoptocl  6896  eroveu  6900  th3qlem1  6911  th3qlem2  6912  th3q  6914  mapsncnv  6977  elixpsn  7017  ixpsnf1o  7018  en1  7086  mapsnend  7099  mapsnen  7100  en2  7112  xpsnen  7119  xpassen  7128  pw2f1odclem  7134  xpf1o  7144  mapen  7146  mapxpen  7148  mapunen  7151  fidifsnen  7172  ac6sfi  7202  undifdc  7231  djuf1olem  7393  djur  7409  updjud  7422  omp1eomlem  7434  0ct  7447  enumctlemm  7454  fodjuomnilemdc  7484  fodjuomni  7489  fodjumkv  7500  nninfwlporlemd  7512  exmidfodomrlemeldju  7551  exmidfodomrlemreseldju  7552  cc2lem  7632  dfplpq2  7721  dfmpq2  7722  enqbreq2  7724  enq0sym  7799  enq0ref  7800  enq0tr  7801  addnq0mo  7814  mulnq0mo  7815  addnnnq0  7816  mulnnnq0  7817  nqnq0a  7821  nqnq0m  7822  nq0a0  7824  prarloclemcalc  7869  genipv  7876  genpassl  7891  genpassu  7892  addcomprg  7945  mulcomprg  7947  distrlem1prl  7949  distrlem1pru  7950  distrlem5prl  7953  distrlem5pru  7954  1idprl  7957  1idpru  7958  recexprlem1ssl  8000  recexprlem1ssu  8001  addsrmo  8110  mulsrmo  8111  addsrpr  8112  mulsrpr  8113  elreal  8195  axcnre  8248  axcaucvglemval  8264  negeu  8518  subeq0  8553  apreap  8917  apreim  8933  divmulap3  9009  diveqap0  9014  diveqap1  9037  nn0ind-raph  9767  elq  10031  zq  10035  elpq  10059  cnref1o  10061  iccf1o  10417  fzen  10457  fseq1m1p1  10512  fzm1  10517  modqmuladd  10816  modqmuladdnn0  10818  modfzo0difsn  10845  nn0ennn  10883  seqf1oglem1  10969  seq3id2  10976  qsqeqor  11100  bcval5  11215  fihashen1  11252  hashf1lem1  11299  wrdl1exs1  11411  wrdl1s1  11412  wrd2ind  11509  swrdccatin2d  11530  reuccatpfxs1lem  11532  shftlem  11595  shftfvalg  11597  shftfval  11600  negfi  12009  xrmaxiflemcom  12031  xrnegiso  12044  xrnegcon1d  12046  sumeq2  12141  summodc  12166  fsum3  12170  fsum2dlemstep  12217  isumsplit  12274  mertenslemub  12317  mertensabs  12320  prodeq2w  12339  prodeq2  12340  prodmodc  12361  fprodseq  12366  fprod2dlemstep  12405  moddvds  12582  modm1div  12583  dvdsnegb  12591  dvdsabseq  12630  dvdsmod  12645  odd2np1lem  12655  odd2np1  12656  opeo  12680  omeo  12681  divalglemnn  12701  divalglemeunn  12704  divalglemex  12705  divalglemeuneg  12706  bitsinv1lem  12744  bezoutlemnewy  12789  bezoutlema  12792  bezoutlemb  12793  bezoutlemex  12794  bezoutlemaz  12796  bezoutlembz  12797  eucalglt  12851  qredeq  12890  qredeu  12891  divgcdcoprm0  12895  divgcdcoprmex  12896  cncongr1  12897  cncongr2  12898  qnumdenbi  12988  nn0sqdcq  13004  hashgcdlem  13036  coprimeprodsq2  13057  pythagtriplem18  13080  pythagtriplem19  13081  pceu  13094  pcval  13095  pczpre  13096  pcdiv  13101  dvdsprmpweq  13134  dvdsprmpweqnn  13135  difsqpwdvds  13137  pcmpt  13142  pcfac  13149  oddprmdvds  13153  4sqlem2  13188  4sqlem3  13189  4sqlem4  13191  4sqlem12  13201  ballotfilemfc0  13281  ballotfilemfcc  13282  evenennn  13333  ennnfonelemim  13364  ptex  13667  intopsn  13736  gzsumvalx  13758  gzsumfzval  13760  gzsumress  13761  gzsumval2  13763  ismnddef  13780  sgrpidmndm  13782  mndpfo  13800  mhmex  13818  grpid  13893  grpidrcan  13919  grpidlcan  13920  grplactcnv  13956  isghm  14095  f1ghm0to0  14124  conjghm  14128  gsumvalfi  14201  srgpcomp  14343  ringadd2  14381  rrgval  14619  opprdomnbg  14632  islmod  14676  lss1d  14769  rspsn  14920  expghmap  14991  zndvds0  15034  znf1o  15035  psrbagconf1o  15113  mplvalcoe  15130  istopon  15163  eltg3  15207  restsn  15330  txuni2  15406  txopn  15415  upxp  15422  uptx  15424  txrest  15426  hmeoimaf1o  15464  xmettxlem  15659  xmettx  15660  elply2  15885  elplyr  15890  zprmlogbaplem3  16136  dvdsppwf1o  16184  mpodvdsmulf1o  16185  perfectlem2  16198  perfect  16199  lgslem1  16217  lgsdirnn0  16264  lgsdinn0  16265  gausslemma2dlem0i  16274  gausslemma2dlem1a  16275  gausslemma2d  16286  lgseisenlem2  16288  lgsquadlem2  16295  2lgslem1b  16306  2lgslem3a1  16314  2lgslem3b1  16315  2lgslem3c1  16316  2lgslem3d1  16317  2lgsoddprmlem2  16323  2sqlem2  16332  2sqlem8  16340  2sqlem9  16341  incistruhgr  16429  upgrex  16442  usgredg4  16554  usgredgreu  16555  uspgredg2vtxeu  16557  uspgredg2v  16560  usgredg2vlem2  16562  usgredg2v  16563  vtxdgfifival  16630  vtxdumgrfival  16637  1loopgrvd2fi  16644  wlk1walkdom  16698  upgriswlkdc  16699  eupth2lem3lem3fi  16809  eupth2fi  16818  bj-nn0suc0  17074  bj-inf2vnlem1  17094  bj-nn0sucALT  17102  pwle2  17126  iooref1o  17181  qdiff  17196