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  2917  rspceeqv  2925  sbceq1g  3144  euabsn  3736  absneu  3738  ifpprsnssdc  3774  preq12bg  3851  cbvopab  4155  cbvopab1  4157  cbvopab2  4158  cbvopab1s  4159  cbvopab2v  4161  mpteq12f  4164  cbvmptf  4178  cbvmpt  4179  exmidsssn  4286  exmidsssnc  4287  opth  4323  eqvinop  4329  moop2  4338  euotd  4341  eusvnf  4544  reusv3i  4550  nlimsucg  4658  nn0suc  4696  opelxp  4749  elvvv  4782  relop  4872  elrnmpt1s  4974  elrnmpt1  4975  elsnres  5042  elxp4  5216  elxp5  5217  relresfld  5258  iotajust  5277  iota1  5293  iota2df  5304  funopg  5352  funcnvuni  5390  fun11iun  5595  funcocnv2  5599  nfvres  5665  ssimaex  5697  fvmptg  5712  fvmptdf  5724  fvopab6  5733  fnmptfvd  5741  fmptco  5803  fsng  5810  funopsn  5819  foco2  5883  elabrex  5887  elabrexg  5888  abrexco  5889  f1veqaeq  5899  dff13f  5900  f1ocnvfv  5909  f1ocnvfvb  5910  fcofo  5914  fliftfun  5926  fliftval  5930  f1oiso2  5957  riotaeqimp  5985  riota5f  5987  oprabid  6039  rspceov  6050  dfoprab2  6057  mpoeq123dva  6071  mpoeq3dva  6074  cbvoprab1  6082  cbvoprab2  6083  cbvoprab12  6084  cbvmpox  6088  mpomptx  6101  ovmpos  6134  ovmpodf  6142  ovmpodv2  6144  ovi3  6148  ov6g  6149  fnrnov  6157  foov  6158  caovcang  6173  caovcan  6176  f1opw2  6218  opabex3d  6272  opabex3  6273  fo1st  6309  fo2nd  6310  elxp6  6321  op1steq  6331  dfoprab4f  6345  fmpox  6352  fnmpoovd  6367  df1st2  6371  df2nd2  6372  xporderlem  6383  cnvoprab  6386  f1od2  6387  brtpos2  6403  dftpos4  6415  tposfn2  6418  recseq  6458  tfr1onlemaccex  6500  tfrcllemaccex  6513  frecabcl  6551  frecsuc  6559  nna0r  6632  eqerlem  6719  qseq2  6739  ecelqsg  6743  snec  6751  qsinxp  6766  ecoptocl  6777  eroveu  6781  th3qlem1  6792  th3qlem2  6793  th3q  6795  mapsncnv  6850  elixpsn  6890  ixpsnf1o  6891  en1  6959  mapsnen  6972  en2  6981  xpsnen  6988  xpassen  6997  pw2f1odclem  7003  xpf1o  7013  mapen  7015  mapxpen  7017  fidifsnen  7040  ac6sfi  7068  undifdc  7097  djuf1olem  7231  djur  7247  updjud  7260  omp1eomlem  7272  0ct  7285  enumctlemm  7292  fodjuomnilemdc  7322  fodjuomni  7327  fodjumkv  7338  nninfwlporlemd  7350  exmidfodomrlemeldju  7388  exmidfodomrlemreseldju  7389  cc2lem  7463  dfplpq2  7552  dfmpq2  7553  enqbreq2  7555  enq0sym  7630  enq0ref  7631  enq0tr  7632  addnq0mo  7645  mulnq0mo  7646  addnnnq0  7647  mulnnnq0  7648  nqnq0a  7652  nqnq0m  7653  nq0a0  7655  prarloclemcalc  7700  genipv  7707  genpassl  7722  genpassu  7723  addcomprg  7776  mulcomprg  7778  distrlem1prl  7780  distrlem1pru  7781  distrlem5prl  7784  distrlem5pru  7785  1idprl  7788  1idpru  7789  recexprlem1ssl  7831  recexprlem1ssu  7832  addsrmo  7941  mulsrmo  7942  addsrpr  7943  mulsrpr  7944  elreal  8026  axcnre  8079  axcaucvglemval  8095  negeu  8348  subeq0  8383  apreap  8745  apreim  8761  divmulap3  8835  diveqap0  8840  diveqap1  8863  nn0ind-raph  9575  elq  9829  zq  9833  elpq  9856  cnref1o  9858  iccf1o  10212  fzen  10251  fseq1m1p1  10303  fzm1  10308  modqmuladd  10600  modqmuladdnn0  10602  modfzo0difsn  10629  nn0ennn  10667  seqf1oglem1  10753  seq3id2  10760  qsqeqor  10884  bcval5  10997  fihashen1  11033  wrdl1exs1  11177  wrdl1s1  11178  wrd2ind  11270  swrdccatin2d  11291  reuccatpfxs1lem  11293  shftlem  11342  shftfvalg  11344  shftfval  11347  negfi  11754  xrmaxiflemcom  11775  xrnegiso  11788  xrnegcon1d  11790  sumeq2  11885  summodc  11909  fsum3  11913  fsum2dlemstep  11960  isumsplit  12017  mertenslemub  12060  mertensabs  12063  prodeq2w  12082  prodeq2  12083  prodmodc  12104  fprodseq  12109  fprod2dlemstep  12148  moddvds  12325  modm1div  12326  dvdsnegb  12334  dvdsabseq  12373  dvdsmod  12388  odd2np1lem  12398  odd2np1  12399  opeo  12423  omeo  12424  divalglemnn  12444  divalglemeunn  12447  divalglemex  12448  divalglemeuneg  12449  bitsinv1lem  12487  bezoutlemnewy  12532  bezoutlema  12535  bezoutlemb  12536  bezoutlemex  12537  bezoutlemaz  12539  bezoutlembz  12540  eucalglt  12594  qredeq  12633  qredeu  12634  divgcdcoprm0  12638  divgcdcoprmex  12639  cncongr1  12640  cncongr2  12641  qnumdenbi  12729  hashgcdlem  12775  coprimeprodsq2  12796  pythagtriplem18  12819  pythagtriplem19  12820  pceu  12833  pcval  12834  pczpre  12835  pcdiv  12840  dvdsprmpweq  12873  dvdsprmpweqnn  12874  difsqpwdvds  12876  pcmpt  12881  pcfac  12888  oddprmdvds  12892  4sqlem2  12927  4sqlem3  12928  4sqlem4  12930  4sqlem12  12940  evenennn  12979  ennnfonelemim  13010  ptex  13312  intopsn  13415  igsumvalx  13437  gsumfzval  13439  gsumpropd  13440  gsumpropd2  13441  gsumress  13443  gsumval2  13445  ismnddef  13466  sgrpidmndm  13468  mndpfo  13486  mhmex  13510  grpid  13587  grpidrcan  13613  grpidlcan  13614  grplactcnv  13650  isghm  13795  f1ghm0to0  13824  conjghm  13828  srgpcomp  13968  ringadd2  14005  rrgval  14241  opprdomnbg  14253  islmod  14270  lss1d  14362  rspsn  14513  expghmap  14586  zndvds0  14629  znf1o  14630  mplvalcoe  14669  istopon  14702  eltg3  14746  restsn  14869  txuni2  14945  txopn  14954  upxp  14961  uptx  14963  txrest  14965  hmeoimaf1o  15003  xmettxlem  15198  xmettx  15199  elply2  15424  elplyr  15429  dvdsppwf1o  15678  mpodvdsmulf1o  15679  perfectlem2  15689  perfect  15690  lgslem1  15694  lgsdirnn0  15741  lgsdinn0  15742  gausslemma2dlem0i  15751  gausslemma2dlem1a  15752  gausslemma2d  15763  lgseisenlem2  15765  lgsquadlem2  15772  2lgslem1b  15783  2lgslem3a1  15791  2lgslem3b1  15792  2lgslem3c1  15793  2lgslem3d1  15794  2lgsoddprmlem2  15800  2sqlem2  15809  2sqlem8  15817  2sqlem9  15818  incistruhgr  15905  upgrex  15918  usgredg4  16028  usgredgreu  16029  uspgredg2vtxeu  16031  uspgredg2v  16034  usgredg2vlem2  16036  usgredg2v  16037  vtxdgfifival  16050  vtxdumgrfival  16057  wlk1walkdom  16100  upgriswlkdc  16101  bj-nn0suc0  16368  bj-inf2vnlem1  16388  bj-nn0sucALT  16396  pwle2  16423  iooref1o  16462