Theorem eqeq2d 2243

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

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

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  eqtrd  2264  eq2tri  2291  rspcedeq2vd  2920  rspceeqv  2928  sbceq1g  3147  euabsn  3741  absneu  3743  ifpprsnssdc  3779  preq12bg  3856  cbvopab  4160  cbvopab1  4162  cbvopab2  4163  cbvopab1s  4164  cbvopab2v  4166  mpteq12f  4169  cbvmptf  4183  cbvmpt  4184  exmidsssn  4292  exmidsssnc  4293  opth  4329  eqvinop  4335  moop2  4344  euotd  4347  eusvnf  4550  reusv3i  4556  nlimsucg  4664  nn0suc  4702  opelxp  4755  elvvv  4789  relop  4880  elrnmpt1s  4982  elrnmpt1  4983  elsnres  5050  elxp4  5224  elxp5  5225  relresfld  5266  iotajust  5285  iota1  5301  iota2df  5312  funopg  5360  funcnvuni  5399  fun11iun  5604  funcocnv2  5608  nfvres  5675  ssimaex  5707  fvmptg  5722  fvmptdf  5734  fvopab6  5743  fnmptfvd  5751  fmptco  5813  fsng  5820  funopsn  5829  foco2  5893  elabrex  5897  elabrexg  5898  abrexco  5899  f1veqaeq  5909  dff13f  5910  f1ocnvfv  5919  f1ocnvfvb  5920  fcofo  5924  fliftfun  5936  fliftval  5940  f1oiso2  5967  riotaeqimp  5995  riota5f  5997  oprabid  6049  rspceov  6060  dfoprab2  6067  mpoeq123dva  6081  mpoeq3dva  6084  cbvoprab1  6092  cbvoprab2  6093  cbvoprab12  6094  cbvmpox  6098  mpomptx  6111  ovmpos  6144  ovmpodf  6152  ovmpodv2  6154  ovi3  6158  ov6g  6159  fnrnov  6167  foov  6168  caovcang  6183  caovcan  6186  f1opw2  6228  opabex3d  6282  opabex3  6283  fo1st  6319  fo2nd  6320  elxp6  6331  op1steq  6341  dfoprab4f  6355  fmpox  6364  fnmpoovd  6379  df1st2  6383  df2nd2  6384  xporderlem  6395  cnvoprab  6398  f1od2  6399  brtpos2  6416  dftpos4  6428  tposfn2  6431  recseq  6471  tfr1onlemaccex  6513  tfrcllemaccex  6526  frecabcl  6564  frecsuc  6572  nna0r  6645  eqerlem  6732  qseq2  6752  ecelqsg  6756  snec  6764  qsinxp  6779  ecoptocl  6790  eroveu  6794  th3qlem1  6805  th3qlem2  6806  th3q  6808  mapsncnv  6863  elixpsn  6903  ixpsnf1o  6904  en1  6972  mapsnen  6985  en2  6997  xpsnen  7004  xpassen  7013  pw2f1odclem  7019  xpf1o  7029  mapen  7031  mapxpen  7033  fidifsnen  7056  ac6sfi  7086  undifdc  7115  djuf1olem  7251  djur  7267  updjud  7280  omp1eomlem  7292  0ct  7305  enumctlemm  7312  fodjuomnilemdc  7342  fodjuomni  7347  fodjumkv  7358  nninfwlporlemd  7370  exmidfodomrlemeldju  7409  exmidfodomrlemreseldju  7410  cc2lem  7484  dfplpq2  7573  dfmpq2  7574  enqbreq2  7576  enq0sym  7651  enq0ref  7652  enq0tr  7653  addnq0mo  7666  mulnq0mo  7667  addnnnq0  7668  mulnnnq0  7669  nqnq0a  7673  nqnq0m  7674  nq0a0  7676  prarloclemcalc  7721  genipv  7728  genpassl  7743  genpassu  7744  addcomprg  7797  mulcomprg  7799  distrlem1prl  7801  distrlem1pru  7802  distrlem5prl  7805  distrlem5pru  7806  1idprl  7809  1idpru  7810  recexprlem1ssl  7852  recexprlem1ssu  7853  addsrmo  7962  mulsrmo  7963  addsrpr  7964  mulsrpr  7965  elreal  8047  axcnre  8100  axcaucvglemval  8116  negeu  8369  subeq0  8404  apreap  8766  apreim  8782  divmulap3  8856  diveqap0  8861  diveqap1  8884  nn0ind-raph  9596  elq  9855  zq  9859  elpq  9882  cnref1o  9884  iccf1o  10238  fzen  10277  fseq1m1p1  10329  fzm1  10334  modqmuladd  10627  modqmuladdnn0  10629  modfzo0difsn  10656  nn0ennn  10694  seqf1oglem1  10780  seq3id2  10787  qsqeqor  10911  bcval5  11024  fihashen1  11060  wrdl1exs1  11205  wrdl1s1  11206  wrd2ind  11303  swrdccatin2d  11324  reuccatpfxs1lem  11326  shftlem  11376  shftfvalg  11378  shftfval  11381  negfi  11788  xrmaxiflemcom  11809  xrnegiso  11822  xrnegcon1d  11824  sumeq2  11919  summodc  11943  fsum3  11947  fsum2dlemstep  11994  isumsplit  12051  mertenslemub  12094  mertensabs  12097  prodeq2w  12116  prodeq2  12117  prodmodc  12138  fprodseq  12143  fprod2dlemstep  12182  moddvds  12359  modm1div  12360  dvdsnegb  12368  dvdsabseq  12407  dvdsmod  12422  odd2np1lem  12432  odd2np1  12433  opeo  12457  omeo  12458  divalglemnn  12478  divalglemeunn  12481  divalglemex  12482  divalglemeuneg  12483  bitsinv1lem  12521  bezoutlemnewy  12566  bezoutlema  12569  bezoutlemb  12570  bezoutlemex  12571  bezoutlemaz  12573  bezoutlembz  12574  eucalglt  12628  qredeq  12667  qredeu  12668  divgcdcoprm0  12672  divgcdcoprmex  12673  cncongr1  12674  cncongr2  12675  qnumdenbi  12763  hashgcdlem  12809  coprimeprodsq2  12830  pythagtriplem18  12853  pythagtriplem19  12854  pceu  12867  pcval  12868  pczpre  12869  pcdiv  12874  dvdsprmpweq  12907  dvdsprmpweqnn  12908  difsqpwdvds  12910  pcmpt  12915  pcfac  12922  oddprmdvds  12926  4sqlem2  12961  4sqlem3  12962  4sqlem4  12964  4sqlem12  12974  evenennn  13013  ennnfonelemim  13044  ptex  13346  intopsn  13449  igsumvalx  13471  gsumfzval  13473  gsumpropd  13474  gsumpropd2  13475  gsumress  13477  gsumval2  13479  ismnddef  13500  sgrpidmndm  13502  mndpfo  13520  mhmex  13544  grpid  13621  grpidrcan  13647  grpidlcan  13648  grplactcnv  13684  isghm  13829  f1ghm0to0  13858  conjghm  13862  srgpcomp  14002  ringadd2  14039  rrgval  14275  opprdomnbg  14287  islmod  14304  lss1d  14396  rspsn  14547  expghmap  14620  zndvds0  14663  znf1o  14664  mplvalcoe  14703  istopon  14736  eltg3  14780  restsn  14903  txuni2  14979  txopn  14988  upxp  14995  uptx  14997  txrest  14999  hmeoimaf1o  15037  xmettxlem  15232  xmettx  15233  elply2  15458  elplyr  15463  dvdsppwf1o  15712  mpodvdsmulf1o  15713  perfectlem2  15723  perfect  15724  lgslem1  15728  lgsdirnn0  15775  lgsdinn0  15776  gausslemma2dlem0i  15785  gausslemma2dlem1a  15786  gausslemma2d  15797  lgseisenlem2  15799  lgsquadlem2  15806  2lgslem1b  15817  2lgslem3a1  15825  2lgslem3b1  15826  2lgslem3c1  15827  2lgslem3d1  15828  2lgsoddprmlem2  15834  2sqlem2  15843  2sqlem8  15851  2sqlem9  15852  incistruhgr  15940  upgrex  15953  usgredg4  16065  usgredgreu  16066  uspgredg2vtxeu  16068  uspgredg2v  16071  usgredg2vlem2  16073  usgredg2v  16074  vtxdgfifival  16141  vtxdumgrfival  16148  1loopgrvd2fi  16155  wlk1walkdom  16209  upgriswlkdc  16210  bj-nn0suc0  16545  bj-inf2vnlem1  16565  bj-nn0sucALT  16573  pwle2  16599  iooref1o  16638  gfsumval  16680