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 ⊢ (𝜑 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

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

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  eqtrd  2271  eq2tri  2298  rspcedeq2vd  2940  rspceeqv  2948  sbceq1g  3167  ifeqeqxdc  3684  euabsn  3777  absneu  3779  ifpprsnssdc  3815  preq12bg  3893  cbvopab  4197  cbvopab1  4199  cbvopab2  4200  cbvopab1s  4201  cbvopab2v  4203  mpteq12f  4206  cbvmptf  4220  cbvmpt  4221  exmidsssn  4334  exmidsssnc  4335  opth  4372  eqvinop  4378  moop2  4387  euotd  4390  eusvnf  4594  reusv3i  4600  nlimsucg  4708  nn0suc  4746  opelxp  4799  elvvv  4833  relop  4925  elrnmpt1s  5027  elrnmpt1  5028  elsnres  5095  elxp4  5270  elxp5  5271  relresfld  5312  iotajust  5331  iota1  5347  iota2df  5358  funopg  5406  funcnvuni  5445  fun11iun  5655  funcocnv2  5659  nfvres  5726  ssimaex  5758  fvmptg  5775  fvmptdf  5787  fvopab6  5796  fnmptfvd  5804  fmptco  5865  fsng  5872  fsn2g  5874  funopsn  5882  dfimafnf  5945  foco2  5949  elabrex  5953  elabrexg  5954  abrexco  5955  f1veqaeq  5965  dff13f  5966  f1ocnvfv  5975  f1ocnvfvb  5976  fcofo  5980  fliftfun  5992  fliftval  5996  f1oiso2  6023  riotaeqimp  6053  riota5f  6055  oprabid  6107  rspceov  6118  dfoprab2  6125  mpoeq123dva  6139  mpoeq3dva  6142  cbvoprab1  6150  cbvoprab2  6151  cbvoprab12  6152  cbvmpox  6156  mpomptx  6169  ovmpos  6202  ovmpodf  6210  ovmpodv2  6212  ovi3  6216  ov6g  6217  fnrnov  6225  foov  6226  caovcang  6241  caovcan  6244  f1opw2  6286  opabex3d  6340  opabex3  6341  fo1st  6381  fo2nd  6382  elxp6  6393  op1steq  6403  dfoprab4f  6417  fmpox  6426  fnmpoovd  6441  df1st2  6445  df2nd2  6446  xporderlem  6457  cnvoprab  6460  f1od2  6461  brtpos2  6512  dftpos4  6524  tposfn2  6527  recseq  6567  tfr1onlemaccex  6609  tfrcllemaccex  6622  frecabcl  6660  frecsuc  6668  nna0r  6741  eqerlem  6828  qseq2  6848  ecelqsg  6852  snec  6860  qsinxp  6875  ecoptocl  6886  eroveu  6890  th3qlem1  6901  th3qlem2  6902  th3q  6904  mapsncnv  6967  elixpsn  7007  ixpsnf1o  7008  en1  7076  mapsnend  7089  mapsnen  7090  en2  7102  xpsnen  7109  xpassen  7118  pw2f1odclem  7124  xpf1o  7134  mapen  7136  mapxpen  7138  mapunen  7141  fidifsnen  7162  ac6sfi  7192  undifdc  7221  djuf1olem  7383  djur  7399  updjud  7412  omp1eomlem  7424  0ct  7437  enumctlemm  7444  fodjuomnilemdc  7474  fodjuomni  7479  fodjumkv  7490  nninfwlporlemd  7502  exmidfodomrlemeldju  7541  exmidfodomrlemreseldju  7542  cc2lem  7622  dfplpq2  7711  dfmpq2  7712  enqbreq2  7714  enq0sym  7789  enq0ref  7790  enq0tr  7791  addnq0mo  7804  mulnq0mo  7805  addnnnq0  7806  mulnnnq0  7807  nqnq0a  7811  nqnq0m  7812  nq0a0  7814  prarloclemcalc  7859  genipv  7866  genpassl  7881  genpassu  7882  addcomprg  7935  mulcomprg  7937  distrlem1prl  7939  distrlem1pru  7940  distrlem5prl  7943  distrlem5pru  7944  1idprl  7947  1idpru  7948  recexprlem1ssl  7990  recexprlem1ssu  7991  addsrmo  8100  mulsrmo  8101  addsrpr  8102  mulsrpr  8103  elreal  8185  axcnre  8238  axcaucvglemval  8254  negeu  8507  subeq0  8542  apreap  8905  apreim  8921  divmulap3  8997  diveqap0  9002  diveqap1  9025  nn0ind-raph  9742  elq  10001  zq  10005  elpq  10028  cnref1o  10030  iccf1o  10386  fzen  10426  fseq1m1p1  10480  fzm1  10485  modqmuladd  10781  modqmuladdnn0  10783  modfzo0difsn  10810  nn0ennn  10848  seqf1oglem1  10934  seq3id2  10941  qsqeqor  11065  bcval5  11179  fihashen1  11216  hashf1lem1  11263  wrdl1exs1  11375  wrdl1s1  11376  wrd2ind  11473  swrdccatin2d  11494  reuccatpfxs1lem  11496  shftlem  11559  shftfvalg  11561  shftfval  11564  negfi  11972  xrmaxiflemcom  11993  xrnegiso  12006  xrnegcon1d  12008  sumeq2  12103  summodc  12128  fsum3  12132  fsum2dlemstep  12179  isumsplit  12236  mertenslemub  12279  mertensabs  12282  prodeq2w  12301  prodeq2  12302  prodmodc  12323  fprodseq  12328  fprod2dlemstep  12367  moddvds  12544  modm1div  12545  dvdsnegb  12553  dvdsabseq  12592  dvdsmod  12607  odd2np1lem  12617  odd2np1  12618  opeo  12642  omeo  12643  divalglemnn  12663  divalglemeunn  12666  divalglemex  12667  divalglemeuneg  12668  bitsinv1lem  12706  bezoutlemnewy  12751  bezoutlema  12754  bezoutlemb  12755  bezoutlemex  12756  bezoutlemaz  12758  bezoutlembz  12759  eucalglt  12813  qredeq  12852  qredeu  12853  divgcdcoprm0  12857  divgcdcoprmex  12858  cncongr1  12859  cncongr2  12860  qnumdenbi  12948  hashgcdlem  12994  coprimeprodsq2  13015  pythagtriplem18  13038  pythagtriplem19  13039  pceu  13052  pcval  13053  pczpre  13054  pcdiv  13059  dvdsprmpweq  13092  dvdsprmpweqnn  13093  difsqpwdvds  13095  pcmpt  13100  pcfac  13107  oddprmdvds  13111  4sqlem2  13146  4sqlem3  13147  4sqlem4  13149  4sqlem12  13159  ballotfilemfc0  13210  ballotfilemfcc  13211  evenennn  13262  ennnfonelemim  13293  ptex  13595  intopsn  13664  gzsumvalx  13686  gzsumfzval  13688  gzsumress  13689  gzsumval2  13691  ismnddef  13708  sgrpidmndm  13710  mndpfo  13728  mhmex  13746  grpid  13821  grpidrcan  13847  grpidlcan  13848  grplactcnv  13884  isghm  14023  f1ghm0to0  14052  conjghm  14056  gsumvalfi  14129  srgpcomp  14268  ringadd2  14305  rrgval  14543  opprdomnbg  14556  islmod  14600  lss1d  14692  rspsn  14843  expghmap  14914  zndvds0  14957  znf1o  14958  psrbagconf1o  14987  mplvalcoe  15004  istopon  15037  eltg3  15081  restsn  15204  txuni2  15280  txopn  15289  upxp  15296  uptx  15298  txrest  15300  hmeoimaf1o  15338  xmettxlem  15533  xmettx  15534  elply2  15759  elplyr  15764  dvdsppwf1o  16017  mpodvdsmulf1o  16018  perfectlem2  16028  perfect  16029  lgslem1  16033  lgsdirnn0  16080  lgsdinn0  16081  gausslemma2dlem0i  16090  gausslemma2dlem1a  16091  gausslemma2d  16102  lgseisenlem2  16104  lgsquadlem2  16111  2lgslem1b  16122  2lgslem3a1  16130  2lgslem3b1  16131  2lgslem3c1  16132  2lgslem3d1  16133  2lgsoddprmlem2  16139  2sqlem2  16148  2sqlem8  16156  2sqlem9  16157  incistruhgr  16245  upgrex  16258  usgredg4  16370  usgredgreu  16371  uspgredg2vtxeu  16373  uspgredg2v  16376  usgredg2vlem2  16378  usgredg2v  16379  vtxdgfifival  16446  vtxdumgrfival  16453  1loopgrvd2fi  16460  wlk1walkdom  16514  upgriswlkdc  16515  eupth2lem3lem3fi  16625  eupth2fi  16634  bj-nn0suc0  16890  bj-inf2vnlem1  16910  bj-nn0sucALT  16918  pwle2  16942  iooref1o  16988  qdiff  17003