Theorem eqeq2d 2241

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  eqtrd  2262  eq2tri  2289  rspcedeq2vd  2918  rspceeqv  2926  sbceq1g  3145  euabsn  3739  absneu  3741  ifpprsnssdc  3777  preq12bg  3854  cbvopab  4158  cbvopab1  4160  cbvopab2  4161  cbvopab1s  4162  cbvopab2v  4164  mpteq12f  4167  cbvmptf  4181  cbvmpt  4182  exmidsssn  4290  exmidsssnc  4291  opth  4327  eqvinop  4333  moop2  4342  euotd  4345  eusvnf  4548  reusv3i  4554  nlimsucg  4662  nn0suc  4700  opelxp  4753  elvvv  4787  relop  4878  elrnmpt1s  4980  elrnmpt1  4981  elsnres  5048  elxp4  5222  elxp5  5223  relresfld  5264  iotajust  5283  iota1  5299  iota2df  5310  funopg  5358  funcnvuni  5396  fun11iun  5601  funcocnv2  5605  nfvres  5671  ssimaex  5703  fvmptg  5718  fvmptdf  5730  fvopab6  5739  fnmptfvd  5747  fmptco  5809  fsng  5816  funopsn  5825  foco2  5889  elabrex  5893  elabrexg  5894  abrexco  5895  f1veqaeq  5905  dff13f  5906  f1ocnvfv  5915  f1ocnvfvb  5916  fcofo  5920  fliftfun  5932  fliftval  5936  f1oiso2  5963  riotaeqimp  5991  riota5f  5993  oprabid  6045  rspceov  6056  dfoprab2  6063  mpoeq123dva  6077  mpoeq3dva  6080  cbvoprab1  6088  cbvoprab2  6089  cbvoprab12  6090  cbvmpox  6094  mpomptx  6107  ovmpos  6140  ovmpodf  6148  ovmpodv2  6150  ovi3  6154  ov6g  6155  fnrnov  6163  foov  6164  caovcang  6179  caovcan  6182  f1opw2  6224  opabex3d  6278  opabex3  6279  fo1st  6315  fo2nd  6316  elxp6  6327  op1steq  6337  dfoprab4f  6351  fmpox  6360  fnmpoovd  6375  df1st2  6379  df2nd2  6380  xporderlem  6391  cnvoprab  6394  f1od2  6395  brtpos2  6412  dftpos4  6424  tposfn2  6427  recseq  6467  tfr1onlemaccex  6509  tfrcllemaccex  6522  frecabcl  6560  frecsuc  6568  nna0r  6641  eqerlem  6728  qseq2  6748  ecelqsg  6752  snec  6760  qsinxp  6775  ecoptocl  6786  eroveu  6790  th3qlem1  6801  th3qlem2  6802  th3q  6804  mapsncnv  6859  elixpsn  6899  ixpsnf1o  6900  en1  6968  mapsnen  6981  en2  6993  xpsnen  7000  xpassen  7009  pw2f1odclem  7015  xpf1o  7025  mapen  7027  mapxpen  7029  fidifsnen  7052  ac6sfi  7080  undifdc  7109  djuf1olem  7243  djur  7259  updjud  7272  omp1eomlem  7284  0ct  7297  enumctlemm  7304  fodjuomnilemdc  7334  fodjuomni  7339  fodjumkv  7350  nninfwlporlemd  7362  exmidfodomrlemeldju  7400  exmidfodomrlemreseldju  7401  cc2lem  7475  dfplpq2  7564  dfmpq2  7565  enqbreq2  7567  enq0sym  7642  enq0ref  7643  enq0tr  7644  addnq0mo  7657  mulnq0mo  7658  addnnnq0  7659  mulnnnq0  7660  nqnq0a  7664  nqnq0m  7665  nq0a0  7667  prarloclemcalc  7712  genipv  7719  genpassl  7734  genpassu  7735  addcomprg  7788  mulcomprg  7790  distrlem1prl  7792  distrlem1pru  7793  distrlem5prl  7796  distrlem5pru  7797  1idprl  7800  1idpru  7801  recexprlem1ssl  7843  recexprlem1ssu  7844  addsrmo  7953  mulsrmo  7954  addsrpr  7955  mulsrpr  7956  elreal  8038  axcnre  8091  axcaucvglemval  8107  negeu  8360  subeq0  8395  apreap  8757  apreim  8773  divmulap3  8847  diveqap0  8852  diveqap1  8875  nn0ind-raph  9587  elq  9846  zq  9850  elpq  9873  cnref1o  9875  iccf1o  10229  fzen  10268  fseq1m1p1  10320  fzm1  10325  modqmuladd  10618  modqmuladdnn0  10620  modfzo0difsn  10647  nn0ennn  10685  seqf1oglem1  10771  seq3id2  10778  qsqeqor  10902  bcval5  11015  fihashen1  11051  wrdl1exs1  11196  wrdl1s1  11197  wrd2ind  11294  swrdccatin2d  11315  reuccatpfxs1lem  11317  shftlem  11367  shftfvalg  11369  shftfval  11372  negfi  11779  xrmaxiflemcom  11800  xrnegiso  11813  xrnegcon1d  11815  sumeq2  11910  summodc  11934  fsum3  11938  fsum2dlemstep  11985  isumsplit  12042  mertenslemub  12085  mertensabs  12088  prodeq2w  12107  prodeq2  12108  prodmodc  12129  fprodseq  12134  fprod2dlemstep  12173  moddvds  12350  modm1div  12351  dvdsnegb  12359  dvdsabseq  12398  dvdsmod  12413  odd2np1lem  12423  odd2np1  12424  opeo  12448  omeo  12449  divalglemnn  12469  divalglemeunn  12472  divalglemex  12473  divalglemeuneg  12474  bitsinv1lem  12512  bezoutlemnewy  12557  bezoutlema  12560  bezoutlemb  12561  bezoutlemex  12562  bezoutlemaz  12564  bezoutlembz  12565  eucalglt  12619  qredeq  12658  qredeu  12659  divgcdcoprm0  12663  divgcdcoprmex  12664  cncongr1  12665  cncongr2  12666  qnumdenbi  12754  hashgcdlem  12800  coprimeprodsq2  12821  pythagtriplem18  12844  pythagtriplem19  12845  pceu  12858  pcval  12859  pczpre  12860  pcdiv  12865  dvdsprmpweq  12898  dvdsprmpweqnn  12899  difsqpwdvds  12901  pcmpt  12906  pcfac  12913  oddprmdvds  12917  4sqlem2  12952  4sqlem3  12953  4sqlem4  12955  4sqlem12  12965  evenennn  13004  ennnfonelemim  13035  ptex  13337  intopsn  13440  igsumvalx  13462  gsumfzval  13464  gsumpropd  13465  gsumpropd2  13466  gsumress  13468  gsumval2  13470  ismnddef  13491  sgrpidmndm  13493  mndpfo  13511  mhmex  13535  grpid  13612  grpidrcan  13638  grpidlcan  13639  grplactcnv  13675  isghm  13820  f1ghm0to0  13849  conjghm  13853  srgpcomp  13993  ringadd2  14030  rrgval  14266  opprdomnbg  14278  islmod  14295  lss1d  14387  rspsn  14538  expghmap  14611  zndvds0  14654  znf1o  14655  mplvalcoe  14694  istopon  14727  eltg3  14771  restsn  14894  txuni2  14970  txopn  14979  upxp  14986  uptx  14988  txrest  14990  hmeoimaf1o  15028  xmettxlem  15223  xmettx  15224  elply2  15449  elplyr  15454  dvdsppwf1o  15703  mpodvdsmulf1o  15704  perfectlem2  15714  perfect  15715  lgslem1  15719  lgsdirnn0  15766  lgsdinn0  15767  gausslemma2dlem0i  15776  gausslemma2dlem1a  15777  gausslemma2d  15788  lgseisenlem2  15790  lgsquadlem2  15797  2lgslem1b  15808  2lgslem3a1  15816  2lgslem3b1  15817  2lgslem3c1  15818  2lgslem3d1  15819  2lgsoddprmlem2  15825  2sqlem2  15834  2sqlem8  15842  2sqlem9  15843  incistruhgr  15931  upgrex  15944  usgredg4  16054  usgredgreu  16055  uspgredg2vtxeu  16057  uspgredg2v  16060  usgredg2vlem2  16062  usgredg2v  16063  vtxdgfifival  16097  vtxdumgrfival  16104  1loopgrvd2fi  16111  wlk1walkdom  16156  upgriswlkdc  16157  bj-nn0suc0  16481  bj-inf2vnlem1  16501  bj-nn0sucALT  16509  pwle2  16535  iooref1o  16574