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  2933  rspceeqv  2941  sbceq1g  3160  euabsn  3763  absneu  3765  ifpprsnssdc  3801  preq12bg  3879  cbvopab  4183  cbvopab1  4185  cbvopab2  4186  cbvopab1s  4187  cbvopab2v  4189  mpteq12f  4192  cbvmptf  4206  cbvmpt  4207  exmidsssn  4317  exmidsssnc  4318  opth  4355  eqvinop  4361  moop2  4370  euotd  4373  eusvnf  4576  reusv3i  4582  nlimsucg  4690  nn0suc  4728  opelxp  4781  elvvv  4815  relop  4907  elrnmpt1s  5009  elrnmpt1  5010  elsnres  5077  elxp4  5252  elxp5  5253  relresfld  5294  iotajust  5313  iota1  5329  iota2df  5340  funopg  5388  funcnvuni  5427  fun11iun  5637  funcocnv2  5641  nfvres  5708  ssimaex  5740  fvmptg  5755  fvmptdf  5767  fvopab6  5776  fnmptfvd  5784  fmptco  5845  fsng  5852  fsn2g  5854  funopsn  5862  foco2  5928  elabrex  5932  elabrexg  5933  abrexco  5934  f1veqaeq  5944  dff13f  5945  f1ocnvfv  5954  f1ocnvfvb  5955  fcofo  5959  fliftfun  5971  fliftval  5975  f1oiso2  6002  riotaeqimp  6030  riota5f  6032  oprabid  6084  rspceov  6095  dfoprab2  6102  mpoeq123dva  6116  mpoeq3dva  6119  cbvoprab1  6127  cbvoprab2  6128  cbvoprab12  6129  cbvmpox  6133  mpomptx  6146  ovmpos  6179  ovmpodf  6187  ovmpodv2  6189  ovi3  6193  ov6g  6194  fnrnov  6202  foov  6203  caovcang  6218  caovcan  6221  f1opw2  6263  opabex3d  6316  opabex3  6317  fo1st  6353  fo2nd  6354  elxp6  6365  op1steq  6375  dfoprab4f  6389  fmpox  6398  fnmpoovd  6413  df1st2  6417  df2nd2  6418  xporderlem  6429  cnvoprab  6432  f1od2  6433  brtpos2  6484  dftpos4  6496  tposfn2  6499  recseq  6539  tfr1onlemaccex  6581  tfrcllemaccex  6594  frecabcl  6632  frecsuc  6640  nna0r  6713  eqerlem  6800  qseq2  6820  ecelqsg  6824  snec  6832  qsinxp  6847  ecoptocl  6858  eroveu  6862  th3qlem1  6873  th3qlem2  6874  th3q  6876  mapsncnv  6932  elixpsn  6972  ixpsnf1o  6973  en1  7041  mapsnend  7054  mapsnen  7055  en2  7067  xpsnen  7074  xpassen  7083  pw2f1odclem  7089  xpf1o  7099  mapen  7101  mapxpen  7103  mapunen  7106  fidifsnen  7127  ac6sfi  7157  undifdc  7186  djuf1olem  7346  djur  7362  updjud  7375  omp1eomlem  7387  0ct  7400  enumctlemm  7407  fodjuomnilemdc  7437  fodjuomni  7442  fodjumkv  7453  nninfwlporlemd  7465  exmidfodomrlemeldju  7504  exmidfodomrlemreseldju  7505  cc2lem  7582  dfplpq2  7671  dfmpq2  7672  enqbreq2  7674  enq0sym  7749  enq0ref  7750  enq0tr  7751  addnq0mo  7764  mulnq0mo  7765  addnnnq0  7766  mulnnnq0  7767  nqnq0a  7771  nqnq0m  7772  nq0a0  7774  prarloclemcalc  7819  genipv  7826  genpassl  7841  genpassu  7842  addcomprg  7895  mulcomprg  7897  distrlem1prl  7899  distrlem1pru  7900  distrlem5prl  7903  distrlem5pru  7904  1idprl  7907  1idpru  7908  recexprlem1ssl  7950  recexprlem1ssu  7951  addsrmo  8060  mulsrmo  8061  addsrpr  8062  mulsrpr  8063  elreal  8145  axcnre  8198  axcaucvglemval  8214  negeu  8466  subeq0  8501  apreap  8863  apreim  8879  divmulap3  8953  diveqap0  8958  diveqap1  8981  nn0ind-raph  9698  elq  9957  zq  9961  elpq  9984  cnref1o  9986  iccf1o  10341  fzen  10380  fseq1m1p1  10433  fzm1  10438  modqmuladd  10732  modqmuladdnn0  10734  modfzo0difsn  10761  nn0ennn  10799  seqf1oglem1  10885  seq3id2  10892  qsqeqor  11016  bcval5  11129  fihashen1  11166  wrdl1exs1  11321  wrdl1s1  11322  wrd2ind  11419  swrdccatin2d  11440  reuccatpfxs1lem  11442  shftlem  11505  shftfvalg  11507  shftfval  11510  negfi  11917  xrmaxiflemcom  11938  xrnegiso  11951  xrnegcon1d  11953  sumeq2  12048  summodc  12073  fsum3  12077  fsum2dlemstep  12124  isumsplit  12181  mertenslemub  12224  mertensabs  12227  prodeq2w  12246  prodeq2  12247  prodmodc  12268  fprodseq  12273  fprod2dlemstep  12312  moddvds  12489  modm1div  12490  dvdsnegb  12498  dvdsabseq  12537  dvdsmod  12552  odd2np1lem  12562  odd2np1  12563  opeo  12587  omeo  12588  divalglemnn  12608  divalglemeunn  12611  divalglemex  12612  divalglemeuneg  12613  bitsinv1lem  12651  bezoutlemnewy  12696  bezoutlema  12699  bezoutlemb  12700  bezoutlemex  12701  bezoutlemaz  12703  bezoutlembz  12704  eucalglt  12758  qredeq  12797  qredeu  12798  divgcdcoprm0  12802  divgcdcoprmex  12803  cncongr1  12804  cncongr2  12805  qnumdenbi  12893  hashgcdlem  12939  coprimeprodsq2  12960  pythagtriplem18  12983  pythagtriplem19  12984  pceu  12997  pcval  12998  pczpre  12999  pcdiv  13004  dvdsprmpweq  13037  dvdsprmpweqnn  13038  difsqpwdvds  13040  pcmpt  13045  pcfac  13052  oddprmdvds  13056  4sqlem2  13091  4sqlem3  13092  4sqlem4  13094  4sqlem12  13104  ballotfilemfc0  13153  ballotfilemfcc  13154  evenennn  13161  ennnfonelemim  13192  ptex  13494  intopsn  13597  igsumvalx  13619  gsumfzval  13621  gsumpropd  13622  gsumpropd2  13623  gsumress  13625  gsumval2  13627  ismnddef  13648  sgrpidmndm  13650  mndpfo  13668  mhmex  13692  grpid  13769  grpidrcan  13795  grpidlcan  13796  grplactcnv  13832  isghm  13977  f1ghm0to0  14006  conjghm  14010  srgpcomp  14151  ringadd2  14188  rrgval  14424  opprdomnbg  14437  islmod  14456  lss1d  14548  rspsn  14699  expghmap  14772  zndvds0  14815  znf1o  14816  psrbagconf1o  14845  mplvalcoe  14862  istopon  14895  eltg3  14939  restsn  15062  txuni2  15138  txopn  15147  upxp  15154  uptx  15156  txrest  15158  hmeoimaf1o  15196  xmettxlem  15391  xmettx  15392  elply2  15617  elplyr  15622  dvdsppwf1o  15874  mpodvdsmulf1o  15875  perfectlem2  15885  perfect  15886  lgslem1  15890  lgsdirnn0  15937  lgsdinn0  15938  gausslemma2dlem0i  15947  gausslemma2dlem1a  15948  gausslemma2d  15959  lgseisenlem2  15961  lgsquadlem2  15968  2lgslem1b  15979  2lgslem3a1  15987  2lgslem3b1  15988  2lgslem3c1  15989  2lgslem3d1  15990  2lgsoddprmlem2  15996  2sqlem2  16005  2sqlem8  16013  2sqlem9  16014  incistruhgr  16102  upgrex  16115  usgredg4  16227  usgredgreu  16228  uspgredg2vtxeu  16230  uspgredg2v  16233  usgredg2vlem2  16235  usgredg2v  16236  vtxdgfifival  16303  vtxdumgrfival  16310  1loopgrvd2fi  16317  wlk1walkdom  16371  upgriswlkdc  16372  eupth2lem3lem3fi  16482  eupth2fi  16491  bj-nn0suc0  16737  bj-inf2vnlem1  16757  bj-nn0sucALT  16765  pwle2  16789  iooref1o  16835  qdiff  16850  gfsumval  16879