Theorem eqeq2d 2244

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 2242	. 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 2214

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

This theorem is referenced by:  eqtrd  2265  eq2tri  2292  rspcedeq2vd  2931  rspceeqv  2939  sbceq1g  3158  euabsn  3761  absneu  3763  ifpprsnssdc  3799  preq12bg  3877  cbvopab  4181  cbvopab1  4183  cbvopab2  4184  cbvopab1s  4185  cbvopab2v  4187  mpteq12f  4190  cbvmptf  4204  cbvmpt  4205  exmidsssn  4315  exmidsssnc  4316  opth  4353  eqvinop  4359  moop2  4368  euotd  4371  eusvnf  4574  reusv3i  4580  nlimsucg  4688  nn0suc  4726  opelxp  4779  elvvv  4813  relop  4905  elrnmpt1s  5007  elrnmpt1  5008  elsnres  5075  elxp4  5250  elxp5  5251  relresfld  5292  iotajust  5311  iota1  5327  iota2df  5338  funopg  5386  funcnvuni  5425  fun11iun  5635  funcocnv2  5639  nfvres  5706  ssimaex  5738  fvmptg  5753  fvmptdf  5765  fvopab6  5774  fnmptfvd  5782  fmptco  5843  fsng  5850  fsn2g  5852  funopsn  5860  foco2  5926  elabrex  5930  elabrexg  5931  abrexco  5932  f1veqaeq  5942  dff13f  5943  f1ocnvfv  5952  f1ocnvfvb  5953  fcofo  5957  fliftfun  5969  fliftval  5973  f1oiso2  6000  riotaeqimp  6028  riota5f  6030  oprabid  6082  rspceov  6093  dfoprab2  6100  mpoeq123dva  6114  mpoeq3dva  6117  cbvoprab1  6125  cbvoprab2  6126  cbvoprab12  6127  cbvmpox  6131  mpomptx  6144  ovmpos  6177  ovmpodf  6185  ovmpodv2  6187  ovi3  6191  ov6g  6192  fnrnov  6200  foov  6201  caovcang  6216  caovcan  6219  f1opw2  6261  opabex3d  6314  opabex3  6315  fo1st  6351  fo2nd  6352  elxp6  6363  op1steq  6373  dfoprab4f  6387  fmpox  6396  fnmpoovd  6411  df1st2  6415  df2nd2  6416  xporderlem  6427  cnvoprab  6430  f1od2  6431  brtpos2  6482  dftpos4  6494  tposfn2  6497  recseq  6537  tfr1onlemaccex  6579  tfrcllemaccex  6592  frecabcl  6630  frecsuc  6638  nna0r  6711  eqerlem  6798  qseq2  6818  ecelqsg  6822  snec  6830  qsinxp  6845  ecoptocl  6856  eroveu  6860  th3qlem1  6871  th3qlem2  6872  th3q  6874  mapsncnv  6930  elixpsn  6970  ixpsnf1o  6971  en1  7039  mapsnend  7052  mapsnen  7053  en2  7065  xpsnen  7072  xpassen  7081  pw2f1odclem  7087  xpf1o  7097  mapen  7099  mapxpen  7101  mapunen  7104  fidifsnen  7125  ac6sfi  7155  undifdc  7184  djuf1olem  7344  djur  7360  updjud  7373  omp1eomlem  7385  0ct  7398  enumctlemm  7405  fodjuomnilemdc  7435  fodjuomni  7440  fodjumkv  7451  nninfwlporlemd  7463  exmidfodomrlemeldju  7502  exmidfodomrlemreseldju  7503  cc2lem  7580  dfplpq2  7669  dfmpq2  7670  enqbreq2  7672  enq0sym  7747  enq0ref  7748  enq0tr  7749  addnq0mo  7762  mulnq0mo  7763  addnnnq0  7764  mulnnnq0  7765  nqnq0a  7769  nqnq0m  7770  nq0a0  7772  prarloclemcalc  7817  genipv  7824  genpassl  7839  genpassu  7840  addcomprg  7893  mulcomprg  7895  distrlem1prl  7897  distrlem1pru  7898  distrlem5prl  7901  distrlem5pru  7902  1idprl  7905  1idpru  7906  recexprlem1ssl  7948  recexprlem1ssu  7949  addsrmo  8058  mulsrmo  8059  addsrpr  8060  mulsrpr  8061  elreal  8143  axcnre  8196  axcaucvglemval  8212  negeu  8464  subeq0  8499  apreap  8861  apreim  8877  divmulap3  8951  diveqap0  8956  diveqap1  8979  nn0ind-raph  9695  elq  9954  zq  9958  elpq  9981  cnref1o  9983  iccf1o  10338  fzen  10377  fseq1m1p1  10429  fzm1  10434  modqmuladd  10728  modqmuladdnn0  10730  modfzo0difsn  10757  nn0ennn  10795  seqf1oglem1  10881  seq3id2  10888  qsqeqor  11012  bcval5  11125  fihashen1  11162  wrdl1exs1  11317  wrdl1s1  11318  wrd2ind  11415  swrdccatin2d  11436  reuccatpfxs1lem  11438  shftlem  11501  shftfvalg  11503  shftfval  11506  negfi  11913  xrmaxiflemcom  11934  xrnegiso  11947  xrnegcon1d  11949  sumeq2  12044  summodc  12069  fsum3  12073  fsum2dlemstep  12120  isumsplit  12177  mertenslemub  12220  mertensabs  12223  prodeq2w  12242  prodeq2  12243  prodmodc  12264  fprodseq  12269  fprod2dlemstep  12308  moddvds  12485  modm1div  12486  dvdsnegb  12494  dvdsabseq  12533  dvdsmod  12548  odd2np1lem  12558  odd2np1  12559  opeo  12583  omeo  12584  divalglemnn  12604  divalglemeunn  12607  divalglemex  12608  divalglemeuneg  12609  bitsinv1lem  12647  bezoutlemnewy  12692  bezoutlema  12695  bezoutlemb  12696  bezoutlemex  12697  bezoutlemaz  12699  bezoutlembz  12700  eucalglt  12754  qredeq  12793  qredeu  12794  divgcdcoprm0  12798  divgcdcoprmex  12799  cncongr1  12800  cncongr2  12801  qnumdenbi  12889  hashgcdlem  12935  coprimeprodsq2  12956  pythagtriplem18  12979  pythagtriplem19  12980  pceu  12993  pcval  12994  pczpre  12995  pcdiv  13000  dvdsprmpweq  13033  dvdsprmpweqnn  13034  difsqpwdvds  13036  pcmpt  13041  pcfac  13048  oddprmdvds  13052  4sqlem2  13087  4sqlem3  13088  4sqlem4  13090  4sqlem12  13100  evenennn  13144  ennnfonelemim  13175  ptex  13477  intopsn  13580  igsumvalx  13602  gsumfzval  13604  gsumpropd  13605  gsumpropd2  13606  gsumress  13608  gsumval2  13610  ismnddef  13631  sgrpidmndm  13633  mndpfo  13651  mhmex  13675  grpid  13752  grpidrcan  13778  grpidlcan  13779  grplactcnv  13815  isghm  13960  f1ghm0to0  13989  conjghm  13993  srgpcomp  14134  ringadd2  14171  rrgval  14407  opprdomnbg  14420  islmod  14439  lss1d  14531  rspsn  14682  expghmap  14755  zndvds0  14798  znf1o  14799  psrbagconf1o  14828  mplvalcoe  14845  istopon  14878  eltg3  14922  restsn  15045  txuni2  15121  txopn  15130  upxp  15137  uptx  15139  txrest  15141  hmeoimaf1o  15179  xmettxlem  15374  xmettx  15375  elply2  15600  elplyr  15605  dvdsppwf1o  15857  mpodvdsmulf1o  15858  perfectlem2  15868  perfect  15869  lgslem1  15873  lgsdirnn0  15920  lgsdinn0  15921  gausslemma2dlem0i  15930  gausslemma2dlem1a  15931  gausslemma2d  15942  lgseisenlem2  15944  lgsquadlem2  15951  2lgslem1b  15962  2lgslem3a1  15970  2lgslem3b1  15971  2lgslem3c1  15972  2lgslem3d1  15973  2lgsoddprmlem2  15979  2sqlem2  15988  2sqlem8  15996  2sqlem9  15997  incistruhgr  16085  upgrex  16098  usgredg4  16210  usgredgreu  16211  uspgredg2vtxeu  16213  uspgredg2v  16216  usgredg2vlem2  16218  usgredg2v  16219  vtxdgfifival  16286  vtxdumgrfival  16293  1loopgrvd2fi  16300  wlk1walkdom  16354  upgriswlkdc  16355  eupth2lem3lem3fi  16465  eupth2fi  16474  bj-nn0suc0  16720  bj-inf2vnlem1  16740  bj-nn0sucALT  16748  pwle2  16772  iooref1o  16818  qdiff  16833  gfsumval  16862